(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/props".
+include "LambdaDelta-1/subst1/defs.ma".
-include "subst1/defs.ma".
-
-include "subst0/props.ma".
+include "LambdaDelta-1/subst0/props.ma".
theorem subst1_head:
\forall (v: T).(\forall (u1: T).(\forall (u2: T).(\forall (i: nat).((subst1
(TLRef h) (TLRef n) (lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n))
(TLRef (plus h (S n))) (lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n))
(sym_eq nat (S (plus h n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h)
-(plus_comm n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n))
+(plus_sym n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n))
(lift_lref_ge n (S h) n (le_n n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt
n (S h) (S n) (le_n (S n)))) i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T
(TLRef (plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i