[To do: add pairs and destructors; unit and negation...]
-Excercise: construct a proof whose labeling is the combinator S.
+Excercise: construct a proof whose labeling is the combinator S,
+something like this:
+
+ --------- Ax --------- Ax ------- Ax
+ !a --> !a !b --> !b c --> c
+ ----------------------- L-> -------- L!
+ !a,!a->!b --> !b !c --> c
+--------- Ax ---------------------------------- L->
+!a --> !a !a,!b->!c,!a->!b --> c
+------------------------------------------ L->
+ !a,!a,!a->!b->!c,!a->!b --> c
+ ----------------------------- C!
+ !a,!a->!b->!c,!a->!b --> c
+ ------------------------------ L!
+ !a,!a->!b->!c,! (!a->!b) --> c
+ ---------------------------------- L!
+ !a,! (!a->!b->!c),! (!a->!b) --> c
+ ----------------------------------- R!
+ !a,! (!a->!b->!c),! (!a->!b) --> !c
+ ------------------------------------ R->
+ ! (!a->!b->!c),! (!a->!b) --> !a->!c
+ ------------------------------------- R->
+ ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
+ --------------------------------------- R->
+ --> ! (!a->!b)->! (!a->!b->!c)->!a->!c