T).(match us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u
(THeads k ul t))])) in THeads.
+inductive C: Set \def
+| CSort: nat \to C
+| CHead: C \to (K \to (T \to C)).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs".
+
+include "T/defs.ma".
+
+inductive iso: T \to (T \to Prop) \def
+| iso_sort: \forall (n1: nat).(\forall (n2: nat).(iso (TSort n1) (TSort n2)))
+| iso_lref: \forall (i1: nat).(\forall (i2: nat).(iso (TLRef i1) (TLRef i2)))
+| iso_head: \forall (k: K).(\forall (v1: T).(\forall (v2: T).(\forall (t1:
+T).(\forall (t2: T).(iso (THead k v1 t1) (THead k v2 t2)))))).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd".
+
+include "iso/defs.ma".
+
+theorem iso_flats_lref_bind_false:
+ \forall (f: F).(\forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall
+(t: T).(\forall (vs: TList).((iso (THeads (Flat f) vs (TLRef i)) (THead (Bind
+b) v t)) \to (\forall (P: Prop).P)))))))
+\def
+ \lambda (f: F).(\lambda (b: B).(\lambda (i: nat).(\lambda (v: T).(\lambda
+(t: T).(\lambda (vs: TList).(TList_ind (\lambda (t0: TList).((iso (THeads
+(Flat f) t0 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P: Prop).P)))
+(\lambda (H: (iso (TLRef i) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0
+\def (match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_:
+(iso t0 t1)).((eq T t0 (TLRef i)) \to ((eq T t1 (THead (Bind b) v t)) \to
+P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1)
+(TLRef i))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v t))).((let H2
+\def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
+T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
+(THead _ _ _) \Rightarrow False])) I (TLRef i) H0) in (False_ind ((eq T
+(TSort n2) (THead (Bind b) v t)) \to P) H2)) H1))) | (iso_lref i1 i2)
+\Rightarrow (\lambda (H0: (eq T (TLRef i1) (TLRef i))).(\lambda (H1: (eq T
+(TLRef i2) (THead (Bind b) v t))).((let H2 \def (f_equal T nat (\lambda (e:
+T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i1 |
+(TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i1])) (TLRef i1) (TLRef
+i) H0) in (eq_ind nat i (\lambda (_: nat).((eq T (TLRef i2) (THead (Bind b) v
+t)) \to P)) (\lambda (H3: (eq T (TLRef i2) (THead (Bind b) v t))).(let H4
+\def (eq_ind T (TLRef i2) (\lambda (e: T).(match e in T return (\lambda (_:
+T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
+(THead _ _ _) \Rightarrow False])) I (THead (Bind b) v t) H3) in (False_ind P
+H4))) i1 (sym_eq nat i1 i H2))) H1))) | (iso_head k v1 v2 t1 t2) \Rightarrow
+(\lambda (H0: (eq T (THead k v1 t1) (TLRef i))).(\lambda (H1: (eq T (THead k
+v2 t2) (THead (Bind b) v t))).((let H2 \def (eq_ind T (THead k v1 t1)
+(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
+\Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
+True])) I (TLRef i) H0) in (False_ind ((eq T (THead k v2 t2) (THead (Bind b)
+v t)) \to P) H2)) H1)))]) in (H0 (refl_equal T (TLRef i)) (refl_equal T
+(THead (Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_:
+(((iso (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P:
+Prop).P)))).(\lambda (H0: (iso (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef
+i))) (THead (Bind b) v t))).(\lambda (P: Prop).(let H1 \def (match H0 in iso
+return (\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (iso t2 t3)).((eq T t2
+(THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) \to ((eq T t3 (THead
+(Bind b) v t)) \to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H1:
+(eq T (TSort n1) (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef
+i))))).(\lambda (H2: (eq T (TSort n2) (THead (Bind b) v t))).((let H3 \def
+(eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
+T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
+(THead _ _ _) \Rightarrow False])) I (THead (Flat f) t0 (THeads (Flat f) t1
+(TLRef i))) H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P)
+H3)) H2))) | (iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1)
+(THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T
+(TLRef i2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TLRef i1) (\lambda
+(e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
+False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
+(THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in (False_ind ((eq T
+(TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) | (iso_head k v1 v2 t2 t3)
+\Rightarrow (\lambda (H1: (eq T (THead k v1 t2) (THead (Flat f) t0 (THeads
+(Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T (THead k v2 t3) (THead (Bind b)
+v t))).((let H3 \def (f_equal T T (\lambda (e: T).(match e in T return
+(\lambda (_: T).T) with [(TSort _) \Rightarrow t2 | (TLRef _) \Rightarrow t2
+| (THead _ _ t) \Rightarrow t])) (THead k v1 t2) (THead (Flat f) t0 (THeads
+(Flat f) t1 (TLRef i))) H1) in ((let H4 \def (f_equal T T (\lambda (e:
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 |
+(TLRef _) \Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead k v1 t2)
+(THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in ((let H5 \def
+(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with
+[(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _)
+\Rightarrow k])) (THead k v1 t2) (THead (Flat f) t0 (THeads (Flat f) t1
+(TLRef i))) H1) in (eq_ind K (Flat f) (\lambda (k0: K).((eq T v1 t0) \to ((eq
+T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead k0 v2 t3) (THead (Bind
+b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0 (\lambda (_:
+T).((eq T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead (Flat f) v2
+t3) (THead (Bind b) v t)) \to P))) (\lambda (H7: (eq T t2 (THeads (Flat f) t1
+(TLRef i)))).(eq_ind T (THeads (Flat f) t1 (TLRef i)) (\lambda (_: T).((eq T
+(THead (Flat f) v2 t3) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T
+(THead (Flat f) v2 t3) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead
+(Flat f) v2 t3) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop)
+with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _
+_) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
+\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8)
+in (False_ind P H9))) t2 (sym_eq T t2 (THeads (Flat f) t1 (TLRef i)) H7))) v1
+(sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f) H5))) H4)) H3)) H2)))]) in (H1
+(refl_equal T (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) (refl_equal
+T (THead (Bind b) v t))))))))) vs)))))).
+
+theorem iso_flats_flat_bind_false:
+ \forall (f1: F).(\forall (f2: F).(\forall (b: B).(\forall (v: T).(\forall
+(v2: T).(\forall (t: T).(\forall (t2: T).(\forall (vs: TList).((iso (THeads
+(Flat f1) vs (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to (\forall (P:
+Prop).P)))))))))
+\def
+ \lambda (f1: F).(\lambda (f2: F).(\lambda (b: B).(\lambda (v: T).(\lambda
+(v2: T).(\lambda (t: T).(\lambda (t2: T).(\lambda (vs: TList).(TList_ind
+(\lambda (t0: TList).((iso (THeads (Flat f1) t0 (THead (Flat f2) v2 t2))
+(THead (Bind b) v t)) \to (\forall (P: Prop).P))) (\lambda (H: (iso (THead
+(Flat f2) v2 t2) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0 \def
+(match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_: (iso t0
+t1)).((eq T t0 (THead (Flat f2) v2 t2)) \to ((eq T t1 (THead (Bind b) v t))
+\to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1)
+(THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v
+t))).((let H2 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
+\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat f2) v2
+t2) H0) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H2))
+H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: (eq T (TLRef i1) (THead
+(Flat f2) v2 t2))).(\lambda (H1: (eq T (TLRef i2) (THead (Bind b) v
+t))).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat f2) v2
+t2) H0) in (False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H2))
+H1))) | (iso_head k v1 v0 t1 t0) \Rightarrow (\lambda (H0: (eq T (THead k v1
+t1) (THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (THead k v0 t0) (THead
+(Bind b) v t))).((let H2 \def (f_equal T T (\lambda (e: T).(match e in T
+return (\lambda (_: T).T) with [(TSort _) \Rightarrow t1 | (TLRef _)
+\Rightarrow t1 | (THead _ _ t) \Rightarrow t])) (THead k v1 t1) (THead (Flat
+f2) v2 t2) H0) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e in T
+return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _)
+\Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead k v1 t1) (THead (Flat
+f2) v2 t2) H0) in ((let H4 \def (f_equal T K (\lambda (e: T).(match e in T
+return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
+\Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k v1 t1) (THead (Flat
+f2) v2 t2) H0) in (eq_ind K (Flat f2) (\lambda (k0: K).((eq T v1 v2) \to ((eq
+T t1 t2) \to ((eq T (THead k0 v0 t0) (THead (Bind b) v t)) \to P)))) (\lambda
+(H5: (eq T v1 v2)).(eq_ind T v2 (\lambda (_: T).((eq T t1 t2) \to ((eq T
+(THead (Flat f2) v0 t0) (THead (Bind b) v t)) \to P))) (\lambda (H6: (eq T t1
+t2)).(eq_ind T t2 (\lambda (_: T).((eq T (THead (Flat f2) v0 t0) (THead (Bind
+b) v t)) \to P)) (\lambda (H7: (eq T (THead (Flat f2) v0 t0) (THead (Bind b)
+v t))).(let H8 \def (eq_ind T (THead (Flat f2) v0 t0) (\lambda (e: T).(match
+e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
+(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
+(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
+True])])) I (THead (Bind b) v t) H7) in (False_ind P H8))) t1 (sym_eq T t1 t2
+H6))) v1 (sym_eq T v1 v2 H5))) k (sym_eq K k (Flat f2) H4))) H3)) H2))
+H1)))]) in (H0 (refl_equal T (THead (Flat f2) v2 t2)) (refl_equal T (THead
+(Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_: (((iso
+(THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to
+(\forall (P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f1) t0 (THeads (Flat
+f1) t1 (THead (Flat f2) v2 t2))) (THead (Bind b) v t))).(\lambda (P:
+Prop).(let H1 \def (match H0 in iso return (\lambda (t3: T).(\lambda (t4:
+T).(\lambda (_: (iso t3 t4)).((eq T t3 (THead (Flat f1) t0 (THeads (Flat f1)
+t1 (THead (Flat f2) v2 t2)))) \to ((eq T t4 (THead (Bind b) v t)) \to P)))))
+with [(iso_sort n1 n2) \Rightarrow (\lambda (H1: (eq T (TSort n1) (THead
+(Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2:
+(eq T (TSort n2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TSort n1)
+(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
+\Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
+False])) I (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))
+H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H3)) H2))) |
+(iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1) (THead (Flat f1)
+t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2: (eq T
+(TLRef i2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TLRef i1) (\lambda
+(e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
+False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
+(THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in
+(False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) |
+(iso_head k v1 v0 t3 t4) \Rightarrow (\lambda (H1: (eq T (THead k v1 t3)
+(THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda
+(H2: (eq T (THead k v0 t4) (THead (Bind b) v t))).((let H3 \def (f_equal T T
+(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
+\Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t) \Rightarrow t]))
+(THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
+t2))) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e in T return
+(\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1
+| (THead _ t _) \Rightarrow t])) (THead k v1 t3) (THead (Flat f1) t0 (THeads
+(Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in ((let H5 \def (f_equal T K
+(\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _)
+\Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k]))
+(THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
+t2))) H1) in (eq_ind K (Flat f1) (\lambda (k0: K).((eq T v1 t0) \to ((eq T t3
+(THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to ((eq T (THead k0 v0 t4)
+(THead (Bind b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0
+(\lambda (_: T).((eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to
+((eq T (THead (Flat f1) v0 t4) (THead (Bind b) v t)) \to P))) (\lambda (H7:
+(eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))).(eq_ind T (THeads
+(Flat f1) t1 (THead (Flat f2) v2 t2)) (\lambda (_: T).((eq T (THead (Flat f1)
+v0 t4) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T (THead (Flat f1) v0
+t4) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead (Flat f1) v0 t4)
+(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
+\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
+(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False |
+(Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8) in (False_ind P
+H9))) t3 (sym_eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) H7))) v1
+(sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f1) H5))) H4)) H3)) H2)))]) in (H1
+(refl_equal T (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
+t2)))) (refl_equal T (THead (Bind b) v t))))))))) vs)))))))).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props".
+
+include "iso/defs.ma".
+
+theorem iso_trans:
+ \forall (t1: T).(\forall (t2: T).((iso t1 t2) \to (\forall (t3: T).((iso t2
+t3) \to (iso t1 t3)))))
+\def
+ \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (iso t1 t2)).(iso_ind (\lambda
+(t: T).(\lambda (t0: T).(\forall (t3: T).((iso t0 t3) \to (iso t t3)))))
+(\lambda (n1: nat).(\lambda (n2: nat).(\lambda (t3: T).(\lambda (H0: (iso
+(TSort n2) t3)).(let H1 \def (match H0 in iso return (\lambda (t: T).(\lambda
+(t0: T).(\lambda (_: (iso t t0)).((eq T t (TSort n2)) \to ((eq T t0 t3) \to
+(iso (TSort n1) t3)))))) with [(iso_sort n0 n3) \Rightarrow (\lambda (H0: (eq
+T (TSort n0) (TSort n2))).(\lambda (H1: (eq T (TSort n3) t3)).((let H2 \def
+(f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with
+[(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _ _)
+\Rightarrow n0])) (TSort n0) (TSort n2) H0) in (eq_ind nat n2 (\lambda (_:
+nat).((eq T (TSort n3) t3) \to (iso (TSort n1) t3))) (\lambda (H3: (eq T
+(TSort n3) t3)).(eq_ind T (TSort n3) (\lambda (t: T).(iso (TSort n1) t))
+(iso_sort n1 n3) t3 H3)) n0 (sym_eq nat n0 n2 H2))) H1))) | (iso_lref i1 i2)
+\Rightarrow (\lambda (H0: (eq T (TLRef i1) (TSort n2))).(\lambda (H1: (eq T
+(TLRef i2) t3)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e
+in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
+_) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n2) H0) in
+(False_ind ((eq T (TLRef i2) t3) \to (iso (TSort n1) t3)) H2)) H1))) |
+(iso_head k v1 v2 t1 t2) \Rightarrow (\lambda (H0: (eq T (THead k v1 t1)
+(TSort n2))).(\lambda (H1: (eq T (THead k v2 t2) t3)).((let H2 \def (eq_ind T
+(THead k v1 t1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop)
+with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
+_) \Rightarrow True])) I (TSort n2) H0) in (False_ind ((eq T (THead k v2 t2)
+t3) \to (iso (TSort n1) t3)) H2)) H1)))]) in (H1 (refl_equal T (TSort n2))
+(refl_equal T t3))))))) (\lambda (i1: nat).(\lambda (i2: nat).(\lambda (t3:
+T).(\lambda (H0: (iso (TLRef i2) t3)).(let H1 \def (match H0 in iso return
+(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t t0)).((eq T t (TLRef
+i2)) \to ((eq T t0 t3) \to (iso (TLRef i1) t3)))))) with [(iso_sort n1 n2)
+\Rightarrow (\lambda (H0: (eq T (TSort n1) (TLRef i2))).(\lambda (H1: (eq T
+(TSort n2) t3)).((let H2 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e
+in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef
+_) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef i2) H0) in
+(False_ind ((eq T (TSort n2) t3) \to (iso (TLRef i1) t3)) H2)) H1))) |
+(iso_lref i0 i3) \Rightarrow (\lambda (H0: (eq T (TLRef i0) (TLRef
+i2))).(\lambda (H1: (eq T (TLRef i3) t3)).((let H2 \def (f_equal T nat
+(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
+\Rightarrow i0 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i0]))
+(TLRef i0) (TLRef i2) H0) in (eq_ind nat i2 (\lambda (_: nat).((eq T (TLRef
+i3) t3) \to (iso (TLRef i1) t3))) (\lambda (H3: (eq T (TLRef i3) t3)).(eq_ind
+T (TLRef i3) (\lambda (t: T).(iso (TLRef i1) t)) (iso_lref i1 i3) t3 H3)) i0
+(sym_eq nat i0 i2 H2))) H1))) | (iso_head k v1 v2 t1 t2) \Rightarrow (\lambda
+(H0: (eq T (THead k v1 t1) (TLRef i2))).(\lambda (H1: (eq T (THead k v2 t2)
+t3)).((let H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef i2) H0) in
+(False_ind ((eq T (THead k v2 t2) t3) \to (iso (TLRef i1) t3)) H2)) H1)))])
+in (H1 (refl_equal T (TLRef i2)) (refl_equal T t3))))))) (\lambda (k:
+K).(\lambda (v1: T).(\lambda (v2: T).(\lambda (t3: T).(\lambda (t4:
+T).(\lambda (t5: T).(\lambda (H0: (iso (THead k v2 t4) t5)).(let H1 \def
+(match H0 in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_: (iso t
+t0)).((eq T t (THead k v2 t4)) \to ((eq T t0 t5) \to (iso (THead k v1 t3)
+t5)))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1)
+(THead k v2 t4))).(\lambda (H1: (eq T (TSort n2) t5)).((let H2 \def (eq_ind T
+(TSort n1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
+[(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _)
+\Rightarrow False])) I (THead k v2 t4) H0) in (False_ind ((eq T (TSort n2)
+t5) \to (iso (THead k v1 t3) t5)) H2)) H1))) | (iso_lref i1 i2) \Rightarrow
+(\lambda (H0: (eq T (TLRef i1) (THead k v2 t4))).(\lambda (H1: (eq T (TLRef
+i2) t5)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k v2 t4) H0)
+in (False_ind ((eq T (TLRef i2) t5) \to (iso (THead k v1 t3) t5)) H2)) H1)))
+| (iso_head k0 v0 v3 t0 t4) \Rightarrow (\lambda (H0: (eq T (THead k0 v0 t0)
+(THead k v2 t4))).(\lambda (H1: (eq T (THead k0 v3 t4) t5)).((let H2 \def
+(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
+[(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t)
+\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H0) in ((let H3 \def
+(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
+[(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 | (THead _ t _)
+\Rightarrow t])) (THead k0 v0 t0) (THead k v2 t4) H0) in ((let H4 \def
+(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with
+[(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k _ _)
+\Rightarrow k])) (THead k0 v0 t0) (THead k v2 t4) H0) in (eq_ind K k (\lambda
+(k1: K).((eq T v0 v2) \to ((eq T t0 t4) \to ((eq T (THead k1 v3 t4) t5) \to
+(iso (THead k v1 t3) t5))))) (\lambda (H5: (eq T v0 v2)).(eq_ind T v2
+(\lambda (_: T).((eq T t0 t4) \to ((eq T (THead k v3 t4) t5) \to (iso (THead
+k v1 t3) t5)))) (\lambda (H6: (eq T t0 t4)).(eq_ind T t4 (\lambda (_: T).((eq
+T (THead k v3 t4) t5) \to (iso (THead k v1 t3) t5))) (\lambda (H7: (eq T
+(THead k v3 t4) t5)).(eq_ind T (THead k v3 t4) (\lambda (t: T).(iso (THead k
+v1 t3) t)) (iso_head k v1 v3 t3 t4) t5 H7)) t0 (sym_eq T t0 t4 H6))) v0
+(sym_eq T v0 v2 H5))) k0 (sym_eq K k0 k H4))) H3)) H2)) H1)))]) in (H1
+(refl_equal T (THead k v2 t4)) (refl_equal T t5)))))))))) t1 t2 H))).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/r/defs".
+
+include "T/defs.ma".
+
+definition r:
+ K \to (nat \to nat)
+\def
+ \lambda (k: K).(\lambda (i: nat).(match k with [(Bind _) \Rightarrow i |
+(Flat _) \Rightarrow (S i)])).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/r/props".
+
+include "r/defs.ma".
+
+include "s/defs.ma".
+
+theorem r_S:
+ \forall (k: K).(\forall (i: nat).(eq nat (r k (S i)) (S (r k i))))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(eq nat (r k0 (S
+i)) (S (r k0 i))))) (\lambda (b: B).(\lambda (i: nat).(refl_equal nat (S (r
+(Bind b) i))))) (\lambda (f: F).(\lambda (i: nat).(refl_equal nat (S (r (Flat
+f) i))))) k).
+
+theorem r_plus:
+ \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k (plus i j))
+(plus (r k i) j))))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j:
+nat).(eq nat (r k0 (plus i j)) (plus (r k0 i) j))))) (\lambda (b: B).(\lambda
+(i: nat).(\lambda (j: nat).(refl_equal nat (plus (r (Bind b) i) j)))))
+(\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (plus (r
+(Flat f) i) j))))) k).
+
+theorem r_plus_sym:
+ \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (r k (plus i j))
+(plus i (r k j)))))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j:
+nat).(eq nat (r k0 (plus i j)) (plus i (r k0 j)))))) (\lambda (_: B).(\lambda
+(i: nat).(\lambda (j: nat).(refl_equal nat (plus i j))))) (\lambda (_:
+F).(\lambda (i: nat).(\lambda (j: nat).(plus_n_Sm i j)))) k).
+
+theorem r_minus:
+ \forall (i: nat).(\forall (n: nat).((lt n i) \to (\forall (k: K).(eq nat
+(minus (r k i) (S n)) (r k (minus i (S n)))))))
+\def
+ \lambda (i: nat).(\lambda (n: nat).(\lambda (H: (lt n i)).(\lambda (k:
+K).(K_ind (\lambda (k0: K).(eq nat (minus (r k0 i) (S n)) (r k0 (minus i (S
+n))))) (\lambda (_: B).(refl_equal nat (minus i (S n)))) (\lambda (_:
+F).(minus_x_Sy i n H)) k)))).
+
+theorem r_dis:
+ \forall (k: K).(\forall (P: Prop).(((((\forall (i: nat).(eq nat (r k i) i)))
+\to P)) \to (((((\forall (i: nat).(eq nat (r k i) (S i)))) \to P)) \to P)))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (P: Prop).(((((\forall (i:
+nat).(eq nat (r k0 i) i))) \to P)) \to (((((\forall (i: nat).(eq nat (r k0 i)
+(S i)))) \to P)) \to P)))) (\lambda (b: B).(\lambda (P: Prop).(\lambda (H:
+((((\forall (i: nat).(eq nat (r (Bind b) i) i))) \to P))).(\lambda (_:
+((((\forall (i: nat).(eq nat (r (Bind b) i) (S i)))) \to P))).(H (\lambda (i:
+nat).(refl_equal nat i))))))) (\lambda (f: F).(\lambda (P: Prop).(\lambda (_:
+((((\forall (i: nat).(eq nat (r (Flat f) i) i))) \to P))).(\lambda (H0:
+((((\forall (i: nat).(eq nat (r (Flat f) i) (S i)))) \to P))).(H0 (\lambda
+(i: nat).(refl_equal nat (S i)))))))) k).
+
+theorem s_r:
+ \forall (k: K).(\forall (i: nat).(eq nat (s k (r k i)) (S i)))
+\def
+ \lambda (k: K).(match k in K return (\lambda (k0: K).(\forall (i: nat).(eq
+nat (s k0 (r k0 i)) (S i)))) with [(Bind _) \Rightarrow (\lambda (i:
+nat).(refl_equal nat (S i))) | (Flat _) \Rightarrow (\lambda (i:
+nat).(refl_equal nat (S i)))]).
+
+theorem r_arith0:
+ \forall (k: K).(\forall (i: nat).(eq nat (minus (r k (S i)) (S O)) (r k i)))
+\def
+ \lambda (k: K).(\lambda (i: nat).(eq_ind_r nat (S (r k i)) (\lambda (n:
+nat).(eq nat (minus n (S O)) (r k i))) (eq_ind_r nat (r k i) (\lambda (n:
+nat).(eq nat n (r k i))) (refl_equal nat (r k i)) (minus (S (r k i)) (S O))
+(minus_Sx_SO (r k i))) (r k (S i)) (r_S k i))).
+
+theorem r_arith1:
+ \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (minus (r k (S
+i)) (S j)) (minus (r k i) j))))
+\def
+ \lambda (k: K).(\lambda (i: nat).(\lambda (j: nat).(eq_ind_r nat (S (r k i))
+(\lambda (n: nat).(eq nat (minus n (S j)) (minus (r k i) j))) (refl_equal nat
+(minus (r k i) j)) (r k (S i)) (r_S k i)))).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/defs".
+
+include "T/defs.ma".
+
+definition wadd:
+ ((nat \to nat)) \to (nat \to (nat \to nat))
+\def
+ \lambda (f: ((nat \to nat))).(\lambda (w: nat).(\lambda (n: nat).(match n
+with [O \Rightarrow w | (S m) \Rightarrow (f m)]))).
+
+definition weight_map:
+ ((nat \to nat)) \to (T \to nat)
+\def
+ let rec weight_map (f: ((nat \to nat))) (t: T) on t: nat \def (match t with
+[(TSort _) \Rightarrow O | (TLRef n) \Rightarrow (f n) | (THead k u t0)
+\Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr
+\Rightarrow (S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f
+u))) t0))) | Abst \Rightarrow (S (plus (weight_map f u) (weight_map (wadd f
+O) t0))) | Void \Rightarrow (S (plus (weight_map f u) (weight_map (wadd f O)
+t0)))]) | (Flat _) \Rightarrow (S (plus (weight_map f u) (weight_map f
+t0)))])]) in weight_map.
+
+definition weight:
+ T \to nat
+\def
+ weight_map (\lambda (_: nat).O).
+
+definition tlt:
+ T \to (T \to Prop)
+\def
+ \lambda (t1: T).(\lambda (t2: T).(lt (weight t1) (weight t2))).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/props".
+
+include "tlt/defs.ma".
+
+theorem wadd_le:
+ \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
+nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((le v w) \to
+(\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
+\def
+ \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
+((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
+nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
+nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le
+(wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
+
+theorem wadd_lt:
+ \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
+nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to
+(\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
+\def
+ \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
+((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
+nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
+nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0))
+(\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0)))
+n))))))).
+
+theorem wadd_O:
+ \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O)
+\def
+ \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_:
+nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat
+(wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n).
+
+theorem weight_le:
+ \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
+nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t)
+(weight_map g t)))))
+\def
+ \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (f: ((nat \to
+nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
+\to (le (weight_map f t0) (weight_map g t0)))))) (\lambda (n: nat).(\lambda
+(f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall (n:
+nat).(le (f n) (g n))))).(le_n (weight_map g (TSort n))))))) (\lambda (n:
+nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
+((\forall (n: nat).(le (f n) (g n))))).(H n))))) (\lambda (k: K).(K_ind
+(\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat \to nat))).(\forall
+(g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le
+(weight_map f t0) (weight_map g t0)))))) \to (\forall (t1: T).(((\forall (f:
+((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n)
+(g n)))) \to (le (weight_map f t1) (weight_map g t1)))))) \to (\forall (f:
+((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n)
+(g n)))) \to (le (weight_map f (THead k0 t0 t1)) (weight_map g (THead k0 t0
+t1))))))))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (t0:
+T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
+(n: nat).(le (f n) (g n)))) \to (le (weight_map f t0) (weight_map g t0))))))
+\to (\forall (t1: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
+nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1)
+(weight_map g t1)))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
+\to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (match b0 with
+[Abbr \Rightarrow (S (plus (weight_map f t0) (weight_map (wadd f (S
+(weight_map f t0))) t1))) | Abst \Rightarrow (S (plus (weight_map f t0)
+(weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus (weight_map f t0)
+(weight_map (wadd f O) t1)))]) (match b0 with [Abbr \Rightarrow (S (plus
+(weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))) | Abst
+\Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) | Void
+\Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O)
+t1)))])))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
+nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
+\to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
+(H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
+(n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
+t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
+nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
+(weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus
+(weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))
+(plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S
+(weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g
+H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0)))
+(\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0))
+(le_n_S (weight_map f t0) (weight_map g t0) (H f g H1)) n))))))))))))
+(\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g:
+((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f
+t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f:
+((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n)
+(g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat
+\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
+(f n) (g n))))).(le_S_n (S (plus (weight_map f t0) (weight_map (wadd f O)
+t1))) (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) (le_n_S (S
+(plus (weight_map f t0) (weight_map (wadd f O) t1))) (S (plus (weight_map g
+t0) (weight_map (wadd g O) t1))) (le_n_S (plus (weight_map f t0) (weight_map
+(wadd f O) t1)) (plus (weight_map g t0) (weight_map (wadd g O) t1))
+(plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f O)
+t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda
+(n: nat).(wadd_le f g H1 O O (le_n O) n)))))))))))))) (\lambda (t0:
+T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
+nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0)
+(weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: ((nat
+\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g
+n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat
+\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
+(f n) (g n))))).(le_S_n (S (plus (weight_map f t0) (weight_map (wadd f O)
+t1))) (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) (le_n_S (S
+(plus (weight_map f t0) (weight_map (wadd f O) t1))) (S (plus (weight_map g
+t0) (weight_map (wadd g O) t1))) (le_n_S (plus (weight_map f t0) (weight_map
+(wadd f O) t1)) (plus (weight_map g t0) (weight_map (wadd g O) t1))
+(plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f O)
+t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda
+(n: nat).(wadd_le f g H1 O O (le_n O) n)))))))))))))) b)) (\lambda (_:
+F).(\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g:
+((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f
+t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f:
+((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n)
+(g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f0:
+((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n:
+nat).(le (f0 n) (g n))))).(lt_le_S (plus (weight_map f0 t0) (weight_map f0
+t1)) (S (plus (weight_map g t0) (weight_map g t1))) (le_lt_n_Sm (plus
+(weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g
+t1)) (plus_le_compat (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1)
+(weight_map g t1) (H f0 g H1) (H0 f0 g H1)))))))))))) k)) t).
+
+theorem weight_eq:
+ \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
+nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f
+t) (weight_map g t)))))
+\def
+ \lambda (t: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
+nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym
+(weight_map f t) (weight_map g t) (weight_le t f g (\lambda (n:
+nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n)
+(H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0:
+nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
+
+theorem weight_add_O:
+ \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t)
+(weight_map (\lambda (_: nat).O) t))
+\def
+ \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_:
+nat).O) (\lambda (n: nat).(wadd_O n))).
+
+theorem weight_add_S:
+ \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O)
+O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
+\def
+ \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O)
+(wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(le_S_n (wadd (\lambda
+(_: nat).O) O n) (wadd (\lambda (_: nat).O) (S m) n) (le_n_S (wadd (\lambda
+(_: nat).O) O n) (wadd (\lambda (_: nat).O) (S m) n) (wadd_le (\lambda (_:
+nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_O_n (S
+m)) n)))))).
+
+theorem tlt_trans:
+ \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to
+(tlt u t)))))
+\def
+ \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u)
+(weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u)
+(weight v) (weight t) H H0))))).
+
+theorem tlt_head_sx:
+ \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
+(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) (THead
+k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
+(t: T).(lt (weight_map (\lambda (_: nat).O) u) (match b0 with [Abbr
+\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
+(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
+\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
+(\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
+(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
+(u: T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda (_: nat).O) u)) (S
+(plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_:
+nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (le_n_S (S (weight_map
+(\lambda (_: nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u)
+(weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
+u))) t))) (le_n_S (weight_map (\lambda (_: nat).O) u) (plus (weight_map
+(\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map
+(\lambda (_: nat).O) u))) t)) (le_plus_l (weight_map (\lambda (_: nat).O) u)
+(weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
+u))) t))))))) (\lambda (u: T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda
+(_: nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map
+(wadd (\lambda (_: nat).O) O) t))) (le_n_S (S (weight_map (\lambda (_:
+nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
+(\lambda (_: nat).O) O) t))) (le_n_S (weight_map (\lambda (_: nat).O) u)
+(plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_:
+nat).O) O) t)) (le_plus_l (weight_map (\lambda (_: nat).O) u) (weight_map
+(wadd (\lambda (_: nat).O) O) t))))))) (\lambda (u: T).(\lambda (t:
+T).(le_S_n (S (weight_map (\lambda (_: nat).O) u)) (S (plus (weight_map
+(\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))
+(le_n_S (S (weight_map (\lambda (_: nat).O) u)) (S (plus (weight_map (\lambda
+(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t))) (le_n_S
+(weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u)
+(weight_map (wadd (\lambda (_: nat).O) O) t)) (le_plus_l (weight_map (\lambda
+(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t))))))) b))
+(\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_S_n (S (weight_map
+(\lambda (_: nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u)
+(weight_map (\lambda (_: nat).O) t))) (le_n_S (S (weight_map (\lambda (_:
+nat).O) u)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda
+(_: nat).O) t))) (le_n_S (weight_map (\lambda (_: nat).O) u) (plus
+(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
+(le_plus_l (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
+nat).O) t)))))))) k).
+
+theorem tlt_head_dx:
+ \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
+\def
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
+(weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead
+k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
+(t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr
+\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
+(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
+\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
+(\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
+(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
+(u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S
+(weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_:
+nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
+nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S
+(weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
+(weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
+u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd
+(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus
+(weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
+(weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd
+(\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda
+(_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t
+(weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t)
+(weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
+(wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t)))))))
+(\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_:
+nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus
+(weight_map (\lambda (_: nat).O) u) n)))) (le_S_n (S (weight_map (\lambda (_:
+nat).O) t)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda
+(_: nat).O) t))) (le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus
+(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)))
+(le_n_S (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_:
+nat).O) u) (weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map
+(\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))))) (weight_map
+(wadd (\lambda (_: nat).O) O) t) (weight_add_O t)))) (\lambda (u: T).(\lambda
+(t: T).(eq_ind_r nat (weight_map (\lambda (_: nat).O) t) (\lambda (n:
+nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus (weight_map (\lambda
+(_: nat).O) u) n)))) (le_S_n (S (weight_map (\lambda (_: nat).O) t)) (S (plus
+(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)))
+(le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda
+(_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) (le_n_S (weight_map
+(\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map
+(\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u)
+(weight_map (\lambda (_: nat).O) t))))) (weight_map (wadd (\lambda (_:
+nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
+T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda (_: nat).O) t)) (S (plus
+(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)))
+(le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda
+(_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) (le_n_S (weight_map
+(\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map
+(\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u)
+(weight_map (\lambda (_: nat).O) t)))))))) k).
+
+theorem tlt_wf__q_ind:
+ \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P: ((T \to
+Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P
+t))))) P n))) \to (\forall (t: T).(P t)))
+\def
+ let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
+T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
+Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t)
+n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight
+t)))))).
+
+theorem tlt_wf_ind:
+ \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t)
+\to (P v)))) \to (P t)))) \to (\forall (t: T).(P t)))
+\def
+ let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
+T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
+Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v)
+(weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(tlt_wf__q_ind
+(\lambda (t0: T).(P t0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (t0:
+T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0)
+\to (Q (\lambda (t: T).(P t)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat
+(weight t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n: nat).(\forall (m:
+nat).((lt m n) \to (\forall (t: T).((eq nat (weight t) m) \to (P t)))))) H0
+(weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt (weight v) (weight
+t0))).(H2 (weight v) H3 v (refl_equal nat (weight v))))))))))))) t)))).
+
set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/problems".
-include "LambdaDelta-6.ma".
+include "LambdaDelta/theory.ma".
(*
+(* Problem 2: disambiguation errors with these objects *)
+
+iso_trans (in iso/props)
+
+drop1_getl_trans
+
(* Problem 1: does not typecheck a match on an empty type *)
theorem subst0_confluence_neq:
\def
\lambda (t0: T).(\lambda (t1: T).(\lambda (u1: T).(\lambda (i1: nat).(\lambda (H: (subst0 i1 u1 t0 t1)).(subst0_ind (\lambda (n: nat).(\lambda (t: T).(\lambda (t2: T).(\lambda (t3: T).(\forall (t4: T).(\forall (u2: T).(\forall (i2: nat).((subst0 i2 u2 t2 t4) \to ((not (eq nat n i2)) \to (ex2 T (\lambda (t5: T).(subst0 i2 u2 t3 t5)) (\lambda (t5: T).(subst0 n t t4 t5)))))))))))) (\lambda (v: T).(\lambda (i: nat).(\lambda (t2: T).(\lambda (u2: T).(\lambda (i2: nat).(\lambda (H0: (subst0 i2 u2 (TLRef i) t2)).(\lambda (H1: (not (eq nat i i2))).(and_ind (eq nat i i2) (eq T t2 (lift (S i) O u2)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (lift (S i) O v) t)) (\lambda (t: T).(subst0 i v t2 t))) (\lambda (H2: (eq nat i i2)).(\lambda (H3: (eq T t2 (lift (S i) O u2))).(let H4 \def (eq_ind nat i (\lambda (n: nat).(not (eq nat n i2))) H1 i2 H2) in (eq_ind_r T (lift (S i) O u2) (\lambda (t: T).(ex2 T (\lambda (t3: T).(subst0 i2 u2 (lift (S i) O v) t3)) (\lambda (t3: T).(subst0 i v t t3)))) (let H5 \def (match (H4 (refl_equal nat i2)) return (\lambda (_: False).(ex2 T (\lambda (t: T).(subst0 i2 u2 (lift (S i) O v) t)) (\lambda (t: T).(subst0 i v (lift (S i) O u2) t)))) with []) in H5) t2 H3)))) (subst0_gen_lref u2 t2 i2 i H0))))))))) (\lambda (v: T).(\lambda (u2: T).(\lambda (u0: T).(\lambda (i: nat).(\lambda (H0: (subst0 i v u0 u2)).(\lambda (H1: ((\forall (t2: T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 u0 t2) \to ((not (eq nat i i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v t2 t)))))))))).(\lambda (t: T).(\lambda (k: K).(\lambda (t2: T).(\lambda (u3: T).(\lambda (i2: nat).(\lambda (H2: (subst0 i2 u3 (THead k u0 t) t2)).(\lambda (H3: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u4: T).(eq T t2 (THead k u4 t))) (\lambda (u4: T).(subst0 i2 u3 u0 u4))) (ex2 T (\lambda (t3: T).(eq T t2 (THead k u0 t3))) (\lambda (t3: T).(subst0 (s k i2) u3 t t3))) (ex3_2 T T (\lambda (u4: T).(\lambda (t3: T).(eq T t2 (THead k u4 t3)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i2) u3 t t3)))) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (H4: (ex2 T (\lambda (u2: T).(eq T t2 (THead k u2 t))) (\lambda (u2: T).(subst0 i2 u3 u0 u2)))).(ex2_ind T (\lambda (u4: T).(eq T t2 (THead k u4 t))) (\lambda (u4: T).(subst0 i2 u3 u0 u4)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (x: T).(\lambda (H5: (eq T t2 (THead k x t))).(\lambda (H6: (subst0 i2 u3 u0 x)).(eq_ind_r T (THead k x t) (\lambda (t3: T).(ex2 T (\lambda (t4: T).(subst0 i2 u3 (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i v t3 t4)))) (ex2_ind T (\lambda (t3: T).(subst0 i2 u3 u2 t3)) (\lambda (t3: T).(subst0 i v x t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k x t) t3))) (\lambda (x0: T).(\lambda (H7: (subst0 i2 u3 u2 x0)).(\lambda (H8: (subst0 i v x x0)).(ex_intro2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k x t) t3)) (THead k x0 t) (subst0_fst u3 x0 u2 i2 H7 t k) (subst0_fst v x0 x i H8 t k))))) (H1 x u3 i2 H6 H3)) t2 H5)))) H4)) (\lambda (H4: (ex2 T (\lambda (t3: T).(eq T t2 (THead k u0 t3))) (\lambda (t2: T).(subst0 (s k i2) u3 t t2)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead k u0 t3))) (\lambda (t3: T).(subst0 (s k i2) u3 t t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (x: T).(\lambda (H5: (eq T t2 (THead k u0 x))).(\lambda (H6: (subst0 (s k i2) u3 t x)).(eq_ind_r T (THead k u0 x) (\lambda (t3: T).(ex2 T (\lambda (t4: T).(subst0 i2 u3 (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i v t3 t4)))) (ex_intro2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k u0 x) t3)) (THead k u2 x) (subst0_snd k u3 x t i2 H6 u2) (subst0_fst v u2 u0 i H0 x k)) t2 H5)))) H4)) (\lambda (H4: (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i2 u3 u0 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i2) u3 t t2))))).(ex3_2_ind T T (\lambda (u4: T).(\lambda (t3: T).(eq T t2 (THead k u4 t3)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i2) u3 t t3))) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T t2 (THead k x0 x1))).(\lambda (H6: (subst0 i2 u3 u0 x0)).(\lambda (H7: (subst0 (s k i2) u3 t x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t3: T).(ex2 T (\lambda (t4: T).(subst0 i2 u3 (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i v t3 t4)))) (ex2_ind T (\lambda (t3: T).(subst0 i2 u3 u2 t3)) (\lambda (t3: T).(subst0 i v x0 t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k x0 x1) t3))) (\lambda (x: T).(\lambda (H8: (subst0 i2 u3 u2 x)).(\lambda (H9: (subst0 i v x0 x)).(ex_intro2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v (THead k x0 x1) t3)) (THead k x x1) (subst0_both u3 u2 x i2 H8 k t x1 H7) (subst0_fst v x x0 i H9 x1 k))))) (H1 x0 u3 i2 H6 H3)) t2 H5)))))) H4)) (subst0_gen_head k u3 u0 t t2 i2 H2))))))))))))))) (\lambda (k: K).(\lambda (v: T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H0: (subst0 (s k i) v t3 t2)).(\lambda (H1: ((\forall (t4: T).(\forall (u2: T).(\forall (i2: nat).((subst0 i2 u2 t3 t4) \to ((not (eq nat (s k i) i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u2 t2 t)) (\lambda (t: T).(subst0 (s k i) v t4 t)))))))))).(\lambda (u: T).(\lambda (t4: T).(\lambda (u2: T).(\lambda (i2: nat).(\lambda (H2: (subst0 i2 u2 (THead k u t3) t4)).(\lambda (H3: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u3: T).(eq T t4 (THead k u3 t3))) (\lambda (u3: T).(subst0 i2 u2 u u3))) (ex2 T (\lambda (t5: T).(eq T t4 (THead k u t5))) (\lambda (t5: T).(subst0 (s k i2) u2 t3 t5))) (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u2 t3 t5)))) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (H4: (ex2 T (\lambda (u2: T).(eq T t4 (THead k u2 t3))) (\lambda (u3: T).(subst0 i2 u2 u u3)))).(ex2_ind T (\lambda (u3: T).(eq T t4 (THead k u3 t3))) (\lambda (u3: T).(subst0 i2 u2 u u3)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x: T).(\lambda (H5: (eq T t4 (THead k x t3))).(\lambda (H6: (subst0 i2 u2 u x)).(eq_ind_r T (THead k x t3) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u2 (THead k u t2) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex_intro2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k x t3) t)) (THead k x t2) (subst0_fst u2 x u i2 H6 t2 k) (subst0_snd k v t2 t3 i H0 x)) t4 H5)))) H4)) (\lambda (H4: (ex2 T (\lambda (t2: T).(eq T t4 (THead k u t2))) (\lambda (t2: T).(subst0 (s k i2) u2 t3 t2)))).(ex2_ind T (\lambda (t5: T).(eq T t4 (THead k u t5))) (\lambda (t5: T).(subst0 (s k i2) u2 t3 t5)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x: T).(\lambda (H5: (eq T t4 (THead k u x))).(\lambda (H6: (subst0 (s k i2) u2 t3 x)).(eq_ind_r T (THead k u x) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u2 (THead k u t2) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u2 t2 t)) (\lambda (t: T).(subst0 (s k i) v x t)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k u x) t))) (\lambda (x0: T).(\lambda (H7: (subst0 (s k i2) u2 t2 x0)).(\lambda (H8: (subst0 (s k i) v x x0)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k u x) t)) (THead k u x0) (subst0_snd k u2 x0 t2 i2 H7 u) (subst0_snd k v x0 x i H8 u))))) (H1 x u2 (s k i2) H6 (\lambda (H7: (eq nat (s k i) (s k i2))).(H3 (s_inj k i i2 H7))))) t4 H5)))) H4)) (\lambda (H4: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t4 (THead k u2 t2)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i2) u2 t3 t2))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u2 t3 t5))) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T t4 (THead k x0 x1))).(\lambda (H6: (subst0 i2 u2 u x0)).(\lambda (H7: (subst0 (s k i2) u2 t3 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u2 (THead k u t2) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u2 t2 t)) (\lambda (t: T).(subst0 (s k i) v x1 t)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t))) (\lambda (x: T).(\lambda (H8: (subst0 (s k i2) u2 t2 x)).(\lambda (H9: (subst0 (s k i) v x1 x)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t)) (THead k x0 x) (subst0_both u2 u x0 i2 H6 k t2 x H8) (subst0_snd k v x x1 i H9 x0))))) (H1 x1 u2 (s k i2) H7 (\lambda (H8: (eq nat (s k i) (s k i2))).(H3 (s_inj k i i2 H8))))) t4 H5)))))) H4)) (subst0_gen_head k u2 u t3 t4 i2 H2))))))))))))))) (\lambda (v: T).(\lambda (u0: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda (H0: (subst0 i v u0 u2)).(\lambda (H1: ((\forall (t2: T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 u0 t2) \to ((not (eq nat i i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v t2 t)))))))))).(\lambda (k: K).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H2: (subst0 (s k i) v t2 t3)).(\lambda (H3: ((\forall (t4: T).(\forall (u2: T).(\forall (i2: nat).((subst0 i2 u2 t2 t4) \to ((not (eq nat (s k i) i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u2 t3 t)) (\lambda (t: T).(subst0 (s k i) v t4 t)))))))))).(\lambda (t4: T).(\lambda (u3: T).(\lambda (i2: nat).(\lambda (H4: (subst0 i2 u3 (THead k u0 t2) t4)).(\lambda (H5: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u4: T).(eq T t4 (THead k u4 t2))) (\lambda (u4: T).(subst0 i2 u3 u0 u4))) (ex2 T (\lambda (t5: T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i2) u3 t2 t5))) (ex3_2 T T (\lambda (u4: T).(\lambda (t5: T).(eq T t4 (THead k u4 t5)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u3 t2 t5)))) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (H6: (ex2 T (\lambda (u2: T).(eq T t4 (THead k u2 t2))) (\lambda (u2: T).(subst0 i2 u3 u0 u2)))).(ex2_ind T (\lambda (u4: T).(eq T t4 (THead k u4 t2))) (\lambda (u4: T).(subst0 i2 u3 u0 u4)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x: T).(\lambda (H7: (eq T t4 (THead k x t2))).(\lambda (H8: (subst0 i2 u3 u0 x)).(eq_ind_r T (THead k x t2) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v x t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x t2) t))) (\lambda (x0: T).(\lambda (H9: (subst0 i2 u3 u2 x0)).(\lambda (H10: (subst0 i v x x0)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x t2) t)) (THead k x0 t3) (subst0_fst u3 x0 u2 i2 H9 t3 k) (subst0_both v x x0 i H10 k t2 t3 H2))))) (H1 x u3 i2 H8 H5)) t4 H7)))) H6)) (\lambda (H6: (ex2 T (\lambda (t2: T).(eq T t4 (THead k u0 t2))) (\lambda (t3: T).(subst0 (s k i2) u3 t2 t3)))).(ex2_ind T (\lambda (t5: T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i2) u3 t2 t5)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x: T).(\lambda (H7: (eq T t4 (THead k u0 x))).(\lambda (H8: (subst0 (s k i2) u3 t2 x)).(eq_ind_r T (THead k u0 x) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0 (s k i) v x t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k u0 x) t))) (\lambda (x0: T).(\lambda (H9: (subst0 (s k i2) u3 t3 x0)).(\lambda (H10: (subst0 (s k i) v x x0)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k u0 x) t)) (THead k u2 x0) (subst0_snd k u3 x0 t3 i2 H9 u2) (subst0_both v u0 u2 i H0 k x x0 H10))))) (H3 x u3 (s k i2) H8 (\lambda (H9: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H9))))) t4 H7)))) H6)) (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t4 (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i2 u3 u0 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i2) u3 t2 t3))))).(ex3_2_ind T T (\lambda (u4: T).(\lambda (t5: T).(eq T t4 (THead k u4 t5)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u3 t2 t5))) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: (eq T t4 (THead k x0 x1))).(\lambda (H8: (subst0 i2 u3 u0 x0)).(\lambda (H9: (subst0 (s k i2) u3 t2 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v x0 t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t))) (\lambda (x: T).(\lambda (H10: (subst0 i2 u3 u2 x)).(\lambda (H11: (subst0 i v x0 x)).(ex2_ind T (\lambda (t: T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0 (s k i) v x1 t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t))) (\lambda (x2: T).(\lambda (H12: (subst0 (s k i2) u3 t3 x2)).(\lambda (H13: (subst0 (s k i) v x1 x2)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t)) (THead k x x2) (subst0_both u3 u2 x i2 H10 k t3 x2 H12) (subst0_both v x0 x i H11 k x1 x2 H13))))) (H3 x1 u3 (s k i2) H9 (\lambda (H12: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H12)))))))) (H1 x0 u3 i2 H8 H5)) t4 H7)))))) H6)) (subst0_gen_head k u3 u0 t2 t4 i2 H4)))))))))))))))))) i1 u1 t0 t1 H))))).
-(* Problem 2: disambiguation errors with these objects *)
-
-iso_trans drop1_getl_trans
-
(* Problem 3: assertion failure raised by type checker on this object *)
tau1
projects / helm.git / commitdiff