- 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.
- assume n : ℕ.
- the thesis becomes
- (equiv
- (if (eqb i n) then E1 else (X n))
- (subst (X n) E2 i)).
- the thesis becomes
- (equiv
- (if (eqb i n) then E1 else (X n))
- (if (eqb i n) then E2 else (X n))).
- we proceed by cases ...
-
-
-
-
\ No newline at end of file
+ conclude
+ (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
+ (val (subst e1 E1 i) v + val (subst e2 E2 i) v) by H11.
+ conclude
+ (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
+ (val (subst e1 E1 i) v + val (subst e2 E1 i) v) by H22.
+ done.