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))).
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))).
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))).
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))).
(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))))).
(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))))).
theorem iso_flats_lref_bind_false:
\forall (f: F).(\forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall
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)))))).
(\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
False])])) I (THead (Flat f) x0 x1) H2) in (False_ind P H3))))) H1))))))))
vs)))))).
theorem iso_flats_flat_bind_false:
\forall (f1: F).(\forall (f2: F).(\forall (b: B).(\forall (v: T).(\forall
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)))))))).
(_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
False])])) I (THead (Flat f1) x0 x1) H2) in (False_ind P H3))))) H1))))))))
vs)))))))).