(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/iso/defs.ma".
+include "Basic-1/iso/defs.ma".
-include "LambdaDelta-1/tlist/defs.ma".
+include "Basic-1/tlist/defs.ma".
theorem iso_gen_sort:
\forall (u2: T).(\forall (n1: nat).((iso (TSort n1) u2) \to (ex nat (\lambda
with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
_) \Rightarrow True])) I (TSort n1) H1) in (False_ind (ex nat (\lambda (n2:
nat).(eq T (THead k v2 t2) (TSort n2)))) H2)))))))) y u2 H0))) H))).
+(* COMMENTS
+Initial nodes: 321
+END *)
theorem iso_gen_lref:
\forall (u2: T).(\forall (n1: nat).((iso (TLRef n1) u2) \to (ex nat (\lambda
with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
_) \Rightarrow True])) I (TLRef n1) H1) in (False_ind (ex nat (\lambda (n2:
nat).(eq T (THead k v2 t2) (TLRef n2)))) H2)))))))) y u2 H0))) H))).
+(* COMMENTS
+Initial nodes: 321
+END *)
theorem iso_gen_head:
\forall (k: K).(\forall (v1: T).(\forall (t1: T).(\forall (u2: T).((iso
(ex_2_intro T T (\lambda (v3: T).(\lambda (t3: T).(eq T (THead k v2 t2)
(THead k v3 t3)))) v2 t2 (refl_equal T (THead k v2 t2))) k0 H6)))) H3))
H2)))))))) y u2 H0))) H))))).
+(* COMMENTS
+Initial nodes: 545
+END *)
theorem iso_flats_lref_bind_false:
\forall (f: F).(\forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall
(\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
False])])) I (THead (Flat f) x0 x1) H2) in (False_ind P H3))))) H1))))))))
vs)))))).
+(* COMMENTS
+Initial nodes: 391
+END *)
theorem iso_flats_flat_bind_false:
\forall (f1: F).(\forall (f2: F).(\forall (b: B).(\forall (v: T).(\forall
(_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
False])])) I (THead (Flat f1) x0 x1) H2) in (False_ind P H3))))) H1))))))))
vs)))))))).
+(* COMMENTS
+Initial nodes: 461
+END *)