manip trees: more explanation

[lambda.git] / hints / assignment_4_answer_4.mdwn

diff --git a/hints/assignment_4_answer_4.mdwn b/hints/assignment_4_answer_4.mdwn
index 17c8490..c2cd1fd 100644 (file)
--- a/hints/assignment_4_answer_4.mdwn
+++ b/hints/assignment_4_answer_4.mdwn
@@ -13,15 +13,17 @@
                        in
 
 
-       Y1 t1 t2 ~~> elem1 elem1 elem2
+       X1 === Y1 t1 t2 ~~> elem1 elem1 elem2
                         === (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
                         ~~> t1 (elem1 elem1 elem2) (elem2 elem1 elem2)
                        <~~> t1 (Y1 t1 t2) (Y2 t1 t2)
+                        === t1 X1 X2
 
                        and
 
-       Y2 t1 t2 ~~> elem2 elem1 elem2
+       X2 === Y2 t1 t2 ~~> elem2 elem1 elem2
                         === (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
                         ~~> t2 (elem1 elem1 elem2) (elem2 elem1 elem2)
                        <~~> t2 (Y1 t1 t2) (Y2 t1 t2)
+                        === t2 X1 X2