and here is an example of rules of the way you encode rules for implication, introduction, implication, elimination and for all introduction and for all elimination.
