(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1".
+include "LambdaDelta-1/subst1/fwd.ma".
-include "subst1/fwd.ma".
-
-include "subst0/subst0.ma".
+include "LambdaDelta-1/subst0/subst0.ma".
theorem subst1_subst1:
\forall (t1: T).(\forall (t2: T).(\forall (u2: T).(\forall (j: nat).((subst1
(t: T).(subst1 i u t (lift (S O) i t2))) H2 (lift (S O) i t1) H1) in (let H4
\def (sym_eq T (lift (S O) i t2) (lift (S O) i t1) (subst1_gen_lift_eq t1 u
(lift (S O) i t2) (S O) i i (le_n i) (eq_ind_r nat (plus (S O) i) (\lambda
-(n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O)) (plus_comm i (S O)))
+(n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O)) (plus_sym i (S O)))
H3)) in (lift_inj t1 t2 (S O) i H4)))))) (\lambda (t2: T).(\lambda (H1:
(subst0 i u t0 t2)).(\lambda (H2: (eq T t2 (lift (S O) i t1))).(\lambda (t3:
T).(\lambda (H3: (subst1 i u t0 (lift (S O) i t3))).(let H4 \def (eq_ind T t2
T).(subst0 i u t (lift (S O) i t1))) H4 (lift (S O) i t3) H6) in
(subst0_gen_lift_false t3 u (lift (S O) i t1) (S O) i i (le_n i) (eq_ind_r
nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i
-(S O)) (plus_comm i (S O))) H7 (eq T t1 t3)))) (\lambda (t4: T).(\lambda (H6:
+(S O)) (plus_sym i (S O))) H7 (eq T t1 t3)))) (\lambda (t4: T).(\lambda (H6:
(subst0 i u t0 t4)).(\lambda (H7: (eq T t4 (lift (S O) i t3))).(let H8 \def
(eq_ind T t4 (\lambda (t: T).(subst0 i u t0 t)) H6 (lift (S O) i t3) H7) in
(sym_eq T t3 t1 (subst0_confluence_lift t0 t3 u i H8 t1 H4)))))) y0 H5)))