(* This file was automatically generated: do not edit *********************)
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/props".
include "tlist/defs.ma".
ts0))).(H2 (tslen ts1) H3 ts1 (refl_equal nat (tslen ts1))))))))))))) ts)))).
theorem theads_tapp:
- \forall (k: K).(\forall (vs: TList).(\forall (v: T).(\forall (t: T).(eq T
+ \forall (k: K).(\forall (v: T).(\forall (t: T).(\forall (vs: TList).(eq T
(THeads k (TApp vs v) t) (THeads k vs (THead k v t))))))
\def
- \lambda (k: K).(\lambda (vs: TList).(TList_ind (\lambda (t: TList).(\forall
-(v: T).(\forall (t0: T).(eq T (THeads k (TApp t v) t0) (THeads k t (THead k v
-t0)))))) (\lambda (v: T).(\lambda (t: T).(refl_equal T (THead k v t))))
-(\lambda (t: T).(\lambda (t0: TList).(\lambda (H: ((\forall (v: T).(\forall
-(t1: T).(eq T (THeads k (TApp t0 v) t1) (THeads k t0 (THead k v
-t1))))))).(\lambda (v: T).(\lambda (t1: T).(eq_ind_r T (THeads k t0 (THead k
-v t1)) (\lambda (t2: T).(eq T (THead k t t2) (THead k t (THeads k t0 (THead k
-v t1))))) (refl_equal T (THead k t (THeads k t0 (THead k v t1)))) (THeads k
-(TApp t0 v) t1) (H v t1))))))) vs)).
+ \lambda (k: K).(\lambda (v: T).(\lambda (t: T).(\lambda (vs:
+TList).(TList_ind (\lambda (t0: TList).(eq T (THeads k (TApp t0 v) t) (THeads
+k t0 (THead k v t)))) (refl_equal T (THead k v t)) (\lambda (t0: T).(\lambda
+(t1: TList).(\lambda (H: (eq T (THeads k (TApp t1 v) t) (THeads k t1 (THead k
+v t)))).(eq_ind T (THeads k (TApp t1 v) t) (\lambda (t2: T).(eq T (THead k t0
+(THeads k (TApp t1 v) t)) (THead k t0 t2))) (refl_equal T (THead k t0 (THeads
+k (TApp t1 v) t))) (THeads k t1 (THead k v t)) H)))) vs)))).
theorem tcons_tapp_ex:
\forall (ts1: TList).(\forall (t1: T).(ex2_2 TList T (\lambda (ts2:
(TCons t1 x0) x1 (refl_equal TList (TApp (TCons t1 x0) x1)) (refl_equal nat
(tslen (TCons t1 x0)))) (tslen t0) H2) (TCons t t0) H1))))) H0))))))) ts1).
-theorem tlist_ind_rew:
+theorem tlist_ind_rev:
\forall (P: ((TList \to Prop))).((P TNil) \to (((\forall (ts:
TList).(\forall (t: T).((P ts) \to (P (TApp ts t)))))) \to (\forall (ts:
TList).(P ts))))