+case EZero.
+ the thesis becomes (equiv (subst EZero E1 i) (subst EZero E2 i)).
+ the thesis becomes (equiv EZero (subst EZero E2 i)).
+ the thesis becomes (equiv EZero EZero).
+ the thesis becomes (∀v.val EZero v = val EZero v).
+ assume v : (ℕ → ℕ).
+ the thesis becomes (0 = val EZero v).
+ the thesis becomes (0 = 0).
+ done.
+case EOne.
+ the thesis becomes (∀v.val EOne v = val EOne v).
+ assume v : (ℕ → ℕ).
+ the thesis becomes (1 = 1).
+ done.
+case EPlus.
+ assume e1 : F.
+ by induction hypothesis we know (equiv (subst e1 E1 i) (subst e1 E2 i)) (H1).
+ assume e2 : F.
+ by induction hypothesis we know (equiv (subst e2 E1 i) (subst e2 E2 i)) (H2).
+ by H1 we proved (∀v.val (subst e1 E1 i) v = val (subst e1 E2 i) v) (H11).
+ by H2 we proved (∀v.val (subst e2 E1 i) v = val (subst e2 E2 i) v) (H22).
+ the thesis becomes
+ (∀v. val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v =
+ val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v).
+ assume v : (ℕ → ℕ).
+ conclude (val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v)
+ = (val (EPlus (subst e1 E1 i) (subst e2 E2 i)) v).
+ = (val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v) by H22.