(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/tlist/defs.ma".
+include "Basic-1/tlist/defs.ma".
theorem tslt_wf__q_ind:
\forall (P: ((TList \to Prop))).(((\forall (n: nat).((\lambda (P0: ((TList
Prop))).(\lambda (H: ((\forall (n: nat).(\forall (ts: TList).((eq nat (tslen
ts) n) \to (P ts)))))).(\lambda (ts: TList).(H (tslen ts) ts (refl_equal nat
(tslen ts)))))).
+(* COMMENTS
+Initial nodes: 61
+END *)
theorem tslt_wf_ind:
\forall (P: ((TList \to Prop))).(((\forall (ts2: TList).(((\forall (ts1:
(\forall (ts1: TList).((eq nat (tslen ts1) m) \to (P ts1)))))) H0 (tslen ts0)
H1) in (H ts0 (\lambda (ts1: TList).(\lambda (H3: (lt (tslen ts1) (tslen
ts0))).(H2 (tslen ts1) H3 ts1 (refl_equal nat (tslen ts1))))))))))))) ts)))).
+(* COMMENTS
+Initial nodes: 179
+END *)
theorem theads_tapp:
\forall (k: K).(\forall (v: T).(\forall (t: T).(\forall (vs: TList).(eq T
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)))).
+(* COMMENTS
+Initial nodes: 175
+END *)
theorem tcons_tapp_ex:
\forall (ts1: TList).(\forall (t1: T).(ex2_2 TList T (\lambda (ts2:
(\lambda (ts2: TList).(\lambda (_: T).(eq nat (S (tslen x0)) (tslen 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).
+(* COMMENTS
+Initial nodes: 503
+END *)
theorem tlist_ind_rev:
\forall (P: ((TList \to Prop))).((P TNil) \to (((\forall (ts:
t1)) (H0 x0 x1 (H2 x0 (eq_ind nat (tslen t0) (\lambda (n: nat).(lt n (tslen
(TCons t t0)))) (le_n (tslen (TCons t t0))) (tslen x0) H5))) (TCons t t0)
H4))))) H3))))))) ts2)) ts)))).
+(* COMMENTS
+Initial nodes: 273
+END *)