helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta-1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta-1".
  16
  17 include "Base.ma".
  18
  19 inductive B: Set \def
  20 | Abbr: B
  21 | Abst: B
  22 | Void: B.
  23
  24 inductive F: Set \def
  25 | Appl: F
  26 | Cast: F.
  27
  28 inductive K: Set \def
  29 | Bind: B \to K
  30 | Flat: F \to K.
  31
  32 inductive T: Set \def
  33 | TSort: nat \to T
  34 | TLRef: nat \to T
  35 | THead: K \to (T \to (T \to T)).
  36
  37 inductive TList: Set \def
  38 | TNil: TList
  39 | TCons: T \to (TList \to TList).
  40
  41 definition THeads:
  42  K \to (TList \to (T \to T))
  43 \def
  44  let rec THeads (k: K) (us: TList) on us: (T \to T) \def (\lambda (t: T).(match us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u (THeads k ul t))])) in THeads.
  45
  46 definition s:
  47  K \to (nat \to nat)
  48 \def
  49  \lambda (k: K).(\lambda (i: nat).(match k with [(Bind _) \Rightarrow (S i) | (Flat _) \Rightarrow i])).
  50
  51 theorem not_abbr_abst:
  52  not (eq B Abbr Abst)
  53 \def
  54  \lambda (H: (eq B Abbr Abst)).(let H0 \def (eq_ind B Abbr (\lambda (ee: B).(match ee return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False])) I Abst H) in (False_ind False H0)).
  55
  56 theorem not_void_abst:
  57  not (eq B Void Abst)
  58 \def
  59  \lambda (H: (eq B Void Abst)).(let H0 \def (eq_ind B Void (\lambda (ee: B).(match ee return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow True])) I Abst H) in (False_ind False H0)).
  60
  61 theorem terms_props__bind_dec:
  62  \forall (b1: B).(\forall (b2: B).(or (eq B b1 b2) ((eq B b1 b2) \to (\forall (P: Prop).P))))
  63 \def
  64  \lambda (b1: B).(B_ind (\lambda (b: B).(\forall (b2: B).(or (eq B b b2) ((eq B b b2) \to (\forall (P: Prop).P))))) (\lambda (b2: B).(B_ind (\lambda (b: B).(or (eq B Abbr b) ((eq B Abbr b) \to (\forall (P: Prop).P)))) (or_introl (eq B Abbr Abbr) ((eq B Abbr Abbr) \to (\forall (P: Prop).P)) (refl_equal B Abbr)) (or_intror (eq B Abbr Abst) ((eq B Abbr Abst) \to (\forall (P: Prop).P)) (\lambda (H: (eq B Abbr Abst)).(\lambda (P: Prop).(let H0 \def (eq_ind B Abbr (\lambda (ee: B).(match ee return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False])) I Abst H) in (False_ind P H0))))) (or_intror (eq B Abbr Void) ((eq B Abbr Void) \to (\forall (P: Prop).P)) (\lambda (H: (eq B Abbr Void)).(\lambda (P: Prop).(let H0 \def (eq_ind B Abbr (\lambda (ee: B).(match ee return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False])) I Void H) in (False_ind P H0))))) b2)) (\lambda (b2: B).(B_ind (\lambda (b: B).(or (eq B Abst b) ((eq B Abst b) \to (\forall (P: Prop).P)))) (or_intror (eq B Abst Abbr) ((eq B Abst Abbr) \to (\forall (P: Prop).P)) (\lambda (H: (eq B Abst Abbr)).(\lambda (P: Prop).(let H0 \def (eq_ind B Abst (\lambda (ee: B).(match ee return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False])) I Abbr H) in (False_ind P H0))))) (or_introl (eq B Abst Abst) ((eq B Abst Abst) \to (\forall (P: Prop).P)) (refl_equal B Abst)) (or_intror (eq B Abst Void) ((eq B Abst Void) \to (\forall (P: Prop).P)) (\lambda (H: (eq B Abst Void)).(\lambda (P: Prop).(let H0 \def (eq_ind B Abst (\lambda (ee: B).(match ee return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False])) I Void H) in (False_ind P H0))))) b2)) (\lambda (b2: B).(B_ind (\lambda (b: B).(or (eq B Void b) ((eq B Void b) \to (\forall (P: Prop).P)))) (or_intror (eq B Void Abbr) ((eq B Void Abbr) \to (\forall (P: Prop).P)) (\lambda (H: (eq B Void Abbr)).(\lambda (P: Prop).(let H0 \def (eq_ind B Void (\lambda (ee: B).(match ee return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow True])) I Abbr H) in (False_ind P H0))))) (or_intror (eq B Void Abst) ((eq B Void Abst) \to (\forall (P: Prop).P)) (\lambda (H: (eq B Void Abst)).(\lambda (P: Prop).(let H0 \def (eq_ind B Void (\lambda (ee: B).(match ee return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow True])) I Abst H) in (False_ind P H0))))) (or_introl (eq B Void Void) ((eq B Void Void) \to (\forall (P: Prop).P)) (refl_equal B Void)) b2)) b1).
  65
  66 theorem terms_props__flat_dec:
  67  \forall (f1: F).(\forall (f2: F).(or (eq F f1 f2) ((eq F f1 f2) \to (\forall (P: Prop).P))))
  68 \def
  69  \lambda (f1: F).(F_ind (\lambda (f: F).(\forall (f2: F).(or (eq F f f2) ((eq F f f2) \to (\forall (P: Prop).P))))) (\lambda (f2: F).(F_ind (\lambda (f: F).(or (eq F Appl f) ((eq F Appl f) \to (\forall (P: Prop).P)))) (or_introl (eq F Appl Appl) ((eq F Appl Appl) \to (\forall (P: Prop).P)) (refl_equal F Appl)) (or_intror (eq F Appl Cast) ((eq F Appl Cast) \to (\forall (P: Prop).P)) (\lambda (H: (eq F Appl Cast)).(\lambda (P: Prop).(let H0 \def (eq_ind F Appl (\lambda (ee: F).(match ee return (\lambda (_: F).Prop) with [Appl \Rightarrow True | Cast \Rightarrow False])) I Cast H) in (False_ind P H0))))) f2)) (\lambda (f2: F).(F_ind (\lambda (f: F).(or (eq F Cast f) ((eq F Cast f) \to (\forall (P: Prop).P)))) (or_intror (eq F Cast Appl) ((eq F Cast Appl) \to (\forall (P: Prop).P)) (\lambda (H: (eq F Cast Appl)).(\lambda (P: Prop).(let H0 \def (eq_ind F Cast (\lambda (ee: F).(match ee return (\lambda (_: F).Prop) with [Appl \Rightarrow False | Cast \Rightarrow True])) I Appl H) in (False_ind P H0))))) (or_introl (eq F Cast Cast) ((eq F Cast Cast) \to (\forall (P: Prop).P)) (refl_equal F Cast)) f2)) f1).
  70
  71 theorem terms_props__kind_dec:
  72  \forall (k1: K).(\forall (k2: K).(or (eq K k1 k2) ((eq K k1 k2) \to (\forall (P: Prop).P))))
  73 \def
  74  \lambda (k1: K).(K_ind (\lambda (k: K).(\forall (k2: K).(or (eq K k k2) ((eq K k k2) \to (\forall (P: Prop).P))))) (\lambda (b: B).(\lambda (k2: K).(K_ind (\lambda (k: K).(or (eq K (Bind b) k) ((eq K (Bind b) k) \to (\forall (P: Prop).P)))) (\lambda (b0: B).(let H_x \def (terms_props__bind_dec b b0) in (let H \def H_x in (or_ind (eq B b b0) ((eq B b b0) \to (\forall (P: Prop).P)) (or (eq K (Bind b) (Bind b0)) ((eq K (Bind b) (Bind b0)) \to (\forall (P: Prop).P))) (\lambda (H0: (eq B b b0)).(eq_ind B b (\lambda (b1: B).(or (eq K (Bind b) (Bind b1)) ((eq K (Bind b) (Bind b1)) \to (\forall (P: Prop).P)))) (or_introl (eq K (Bind b) (Bind b)) ((eq K (Bind b) (Bind b)) \to (\forall (P: Prop).P)) (refl_equal K (Bind b))) b0 H0)) (\lambda (H0: (((eq B b b0) \to (\forall (P: Prop).P)))).(or_intror (eq K (Bind b) (Bind b0)) ((eq K (Bind b) (Bind b0)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq K (Bind b) (Bind b0))).(\lambda (P: Prop).(let H2 \def (f_equal K B (\lambda (e: K).(match e return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b])) (Bind b) (Bind b0) H1) in (let H3 \def (eq_ind_r B b0 (\lambda (b0: B).((eq B b b0) \to (\forall (P: Prop).P))) H0 b H2) in (H3 (refl_equal B b) P))))))) H)))) (\lambda (f: F).(or_intror (eq K (Bind b) (Flat f)) ((eq K (Bind b) (Flat f)) \to (\forall (P: Prop).P)) (\lambda (H: (eq K (Bind b) (Flat f))).(\lambda (P: Prop).(let H0 \def (eq_ind K (Bind b) (\lambda (ee: K).(match ee return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])) I (Flat f) H) in (False_ind P H0)))))) k2))) (\lambda (f: F).(\lambda (k2: K).(K_ind (\lambda (k: K).(or (eq K (Flat f) k) ((eq K (Flat f) k) \to (\forall (P: Prop).P)))) (\lambda (b: B).(or_intror (eq K (Flat f) (Bind b)) ((eq K (Flat f) (Bind b)) \to (\forall (P: Prop).P)) (\lambda (H: (eq K (Flat f) (Bind b))).(\lambda (P: Prop).(let H0 \def (eq_ind K (Flat f) (\lambda (ee: K).(match ee return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) I (Bind b) H) in (False_ind P H0)))))) (\lambda (f0: F).(let H_x \def (terms_props__flat_dec f f0) in (let H \def H_x in (or_ind (eq F f f0) ((eq F f f0) \to (\forall (P: Prop).P)) (or (eq K (Flat f) (Flat f0)) ((eq K (Flat f) (Flat f0)) \to (\forall (P: Prop).P))) (\lambda (H0: (eq F f f0)).(eq_ind F f (\lambda (f1: F).(or (eq K (Flat f) (Flat f1)) ((eq K (Flat f) (Flat f1)) \to (\forall (P: Prop).P)))) (or_introl (eq K (Flat f) (Flat f)) ((eq K (Flat f) (Flat f)) \to (\forall (P: Prop).P)) (refl_equal K (Flat f))) f0 H0)) (\lambda (H0: (((eq F f f0) \to (\forall (P: Prop).P)))).(or_intror (eq K (Flat f) (Flat f0)) ((eq K (Flat f) (Flat f0)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq K (Flat f) (Flat f0))).(\lambda (P: Prop).(let H2 \def (f_equal K F (\lambda (e: K).(match e return (\lambda (_: K).F) with [(Bind _) \Rightarrow f | (Flat f) \Rightarrow f])) (Flat f) (Flat f0) H1) in (let H3 \def (eq_ind_r F f0 (\lambda (f0: F).((eq F f f0) \to (\forall (P: Prop).P))) H0 f H2) in (H3 (refl_equal F f) P))))))) H)))) k2))) k1).
  75
  76 theorem term_dec:
  77  \forall (t1: T).(\forall (t2: T).(or (eq T t1 t2) ((eq T t1 t2) \to (\forall (P: Prop).P))))
  78 \def
  79  \lambda (t1: T).(T_ind (\lambda (t: T).(\forall (t2: T).(or (eq T t t2) ((eq T t t2) \to (\forall (P: Prop).P))))) (\lambda (n: nat).(\lambda (t2: T).(T_ind (\lambda (t: T).(or (eq T (TSort n) t) ((eq T (TSort n) t) \to (\forall (P: Prop).P)))) (\lambda (n0: nat).(let H_x \def (nat_dec n n0) in (let H \def H_x in (or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P: Prop).P)) (or (eq T (TSort n) (TSort n0)) ((eq T (TSort n) (TSort n0)) \to (\forall (P: Prop).P))) (\lambda (H0: (eq nat n n0)).(eq_ind nat n (\lambda (n1: nat).(or (eq T (TSort n) (TSort n1)) ((eq T (TSort n) (TSort n1)) \to (\forall (P: Prop).P)))) (or_introl (eq T (TSort n) (TSort n)) ((eq T (TSort n) (TSort n)) \to (\forall (P: Prop).P)) (refl_equal T (TSort n))) n0 H0)) (\lambda (H0: (((eq nat n n0) \to (\forall (P: Prop).P)))).(or_intror (eq T (TSort n) (TSort n0)) ((eq T (TSort n) (TSort n0)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (TSort n) (TSort n0))).(\lambda (P: Prop).(let H2 \def (f_equal T nat (\lambda (e: T).(match e return (\lambda (_: T).nat) with [(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n | (THead _ _ _) \Rightarrow n])) (TSort n) (TSort n0) H1) in (let H3 \def (eq_ind_r nat n0 (\lambda (n0: nat).((eq nat n n0) \to (\forall (P: Prop).P))) H0 n H2) in (H3 (refl_equal nat n) P))))))) H)))) (\lambda (n0: nat).(or_intror (eq T (TSort n) (TLRef n0)) ((eq T (TSort n) (TLRef n0)) \to (\forall (P: Prop).P)) (\lambda (H: (eq T (TSort n) (TLRef n0))).(\lambda (P: Prop).(let H0 \def (eq_ind T (TSort n) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef n0) H) in (False_ind P H0)))))) (\lambda (k: K).(\lambda (t: T).(\lambda (_: (or (eq T (TSort n) t) ((eq T (TSort n) t) \to (\forall (P: Prop).P)))).(\lambda (t0: T).(\lambda (_: (or (eq T (TSort n) t0) ((eq T (TSort n) t0) \to (\forall (P: Prop).P)))).(or_intror (eq T (TSort n) (THead k t t0)) ((eq T (TSort n) (THead k t t0)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (TSort n) (THead k t t0))).(\lambda (P: Prop).(let H2 \def (eq_ind T (TSort n) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead k t t0) H1) in (False_ind P H2)))))))))) t2))) (\lambda (n: nat).(\lambda (t2: T).(T_ind (\lambda (t: T).(or (eq T (TLRef n) t) ((eq T (TLRef n) t) \to (\forall (P: Prop).P)))) (\lambda (n0: nat).(or_intror (eq T (TLRef n) (TSort n0)) ((eq T (TLRef n) (TSort n0)) \to (\forall (P: Prop).P)) (\lambda (H: (eq T (TLRef n) (TSort n0))).(\lambda (P: Prop).(let H0 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n0) H) in (False_ind P H0)))))) (\lambda (n0: nat).(let H_x \def (nat_dec n n0) in (let H \def H_x in (or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P: Prop).P)) (or (eq T (TLRef n) (TLRef n0)) ((eq T (TLRef n) (TLRef n0)) \to (\forall (P: Prop).P))) (\lambda (H0: (eq nat n n0)).(eq_ind nat n (\lambda (n1: nat).(or (eq T (TLRef n) (TLRef n1)) ((eq T (TLRef n) (TLRef n1)) \to (\forall (P: Prop).P)))) (or_introl (eq T (TLRef n) (TLRef n)) ((eq T (TLRef n) (TLRef n)) \to (\forall (P: Prop).P)) (refl_equal T (TLRef n))) n0 H0)) (\lambda (H0: (((eq nat n n0) \to (\forall (P: Prop).P)))).(or_intror (eq T (TLRef n) (TLRef n0)) ((eq T (TLRef n) (TLRef n0)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (TLRef n) (TLRef n0))).(\lambda (P: Prop).(let H2 \def (f_equal T nat (\lambda (e: T).(match e return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef n0) H1) in (let H3 \def (eq_ind_r nat n0 (\lambda (n0: nat).((eq nat n n0) \to (\forall (P: Prop).P))) H0 n H2) in (H3 (refl_equal nat n) P))))))) H)))) (\lambda (k: K).(\lambda (t: T).(\lambda (_: (or (eq T (TLRef n) t) ((eq T (TLRef n) t) \to (\forall (P: Prop).P)))).(\lambda (t0: T).(\lambda (_: (or (eq T (TLRef n) t0) ((eq T (TLRef n) t0) \to (\forall (P: Prop).P)))).(or_intror (eq T (TLRef n) (THead k t t0)) ((eq T (TLRef n) (THead k t t0)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (TLRef n) (THead k t t0))).(\lambda (P: Prop).(let H2 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k t t0) H1) in (False_ind P H2)))))))))) t2))) (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (t2: T).(or (eq T t t2) ((eq T t t2) \to (\forall (P: Prop).P)))))).(\lambda (t0: T).(\lambda (H0: ((\forall (t2: T).(or (eq T t0 t2) ((eq T t0 t2) \to (\forall (P: Prop).P)))))).(\lambda (t2: T).(T_ind (\lambda (t3: T).(or (eq T (THead k t t0) t3) ((eq T (THead k t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (n: nat).(or_intror (eq T (THead k t t0) (TSort n)) ((eq T (THead k t t0) (TSort n)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (THead k t t0) (TSort n))).(\lambda (P: Prop).(let H2 \def (eq_ind T (THead k t t0) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H1) in (False_ind P H2)))))) (\lambda (n: nat).(or_intror (eq T (THead k t t0) (TLRef n)) ((eq T (THead k t t0) (TLRef n)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (THead k t t0) (TLRef n))).(\lambda (P: Prop).(let H2 \def (eq_ind T (THead k t t0) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind P H2)))))) (\lambda (k0: K).(\lambda (t3: T).(\lambda (H1: (or (eq T (THead k t t0) t3) ((eq T (THead k t t0) t3) \to (\forall (P: Prop).P)))).(\lambda (t4: T).(\lambda (H2: (or (eq T (THead k t t0) t4) ((eq T (THead k t t0) t4) \to (\forall (P: Prop).P)))).(let H_x \def (H t3) in (let H3 \def H_x in (or_ind (eq T t t3) ((eq T t t3) \to (\forall (P: Prop).P)) (or (eq T (THead k t t0) (THead k0 t3 t4)) ((eq T (THead k t t0) (THead k0 t3 t4)) \to (\forall (P: Prop).P))) (\lambda (H4: (eq T t t3)).(let H5 \def (eq_ind_r T t3 (\lambda (t1: T).(or (eq T (THead k t t0) t1) ((eq T (THead k t t0) t1) \to (\forall (P: Prop).P)))) H1 t H4) in (eq_ind T t (\lambda (t5: T).(or (eq T (THead k t t0) (THead k0 t5 t4)) ((eq T (THead k t t0) (THead k0 t5 t4)) \to (\forall (P: Prop).P)))) (let H_x0 \def (H0 t4) in (let H6 \def H_x0 in (or_ind (eq T t0 t4) ((eq T t0 t4) \to (\forall (P: Prop).P)) (or (eq T (THead k t t0) (THead k0 t t4)) ((eq T (THead k t t0) (THead k0 t t4)) \to (\forall (P: Prop).P))) (\lambda (H7: (eq T t0 t4)).(let H8 \def (eq_ind_r T t4 (\lambda (t1: T).(or (eq T (THead k t t0) t1) ((eq T (THead k t t0) t1) \to (\forall (P: Prop).P)))) H2 t0 H7) in (eq_ind T t0 (\lambda (t5: T).(or (eq T (THead k t t0) (THead k0 t t5)) ((eq T (THead k t t0) (THead k0 t t5)) \to (\forall (P: Prop).P)))) (let H_x1 \def (terms_props__kind_dec k k0) in (let H9 \def H_x1 in (or_ind (eq K k k0) ((eq K k k0) \to (\forall (P: Prop).P)) (or (eq T (THead k t t0) (THead k0 t t0)) ((eq T (THead k t t0) (THead k0 t t0)) \to (\forall (P: Prop).P))) (\lambda (H10: (eq K k k0)).(eq_ind K k (\lambda (k1: K).(or (eq T (THead k t t0) (THead k1 t t0)) ((eq T (THead k t t0) (THead k1 t t0)) \to (\forall (P: Prop).P)))) (or_introl (eq T (THead k t t0) (THead k t t0)) ((eq T (THead k t t0) (THead k t t0)) \to (\forall (P: Prop).P)) (refl_equal T (THead k t t0))) k0 H10)) (\lambda (H10: (((eq K k k0) \to (\forall (P: Prop).P)))).(or_intror (eq T (THead k t t0) (THead k0 t t0)) ((eq T (THead k t t0) (THead k0 t t0)) \to (\forall (P: Prop).P)) (\lambda (H11: (eq T (THead k t t0) (THead k0 t t0))).(\lambda (P: Prop).(let H12 \def (f_equal T K (\lambda (e: T).(match e return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k t t0) (THead k0 t t0) H11) in (let H13 \def (eq_ind_r K k0 (\lambda (k0: K).((eq K k k0) \to (\forall (P: Prop).P))) H10 k H12) in (H13 (refl_equal K k) P))))))) H9))) t4 H7))) (\lambda (H7: (((eq T t0 t4) \to (\forall (P: Prop).P)))).(or_intror (eq T (THead k t t0) (THead k0 t t4)) ((eq T (THead k t t0) (THead k0 t t4)) \to (\forall (P: Prop).P)) (\lambda (H8: (eq T (THead k t t0) (THead k0 t t4))).(\lambda (P: Prop).(let H9 \def (f_equal T K (\lambda (e: T).(match e return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k t t0) (THead k0 t t4) H8) in ((let H10 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k t t0) (THead k0 t t4) H8) in (\lambda (_: (eq K k k0)).(let H12 \def (eq_ind_r T t4 (\lambda (t: T).((eq T t0 t) \to (\forall (P: Prop).P))) H7 t0 H10) in (let H13 \def (eq_ind_r T t4 (\lambda (t1: T).(or (eq T (THead k t t0) t1) ((eq T (THead k t t0) t1) \to (\forall (P: Prop).P)))) H2 t0 H10) in (H12 (refl_equal T t0) P))))) H9)))))) H6))) t3 H4))) (\lambda (H4: (((eq T t t3) \to (\forall (P: Prop).P)))).(or_intror (eq T (THead k t t0) (THead k0 t3 t4)) ((eq T (THead k t t0) (THead k0 t3 t4)) \to (\forall (P: Prop).P)) (\lambda (H5: (eq T (THead k t t0) (THead k0 t3 t4))).(\lambda (P: Prop).(let H6 \def (f_equal T K (\lambda (e: T).(match e return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k t t0) (THead k0 t3 t4) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ t _) \Rightarrow t])) (THead k t t0) (THead k0 t3 t4) H5) in ((let H8 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k t t0) (THead k0 t3 t4) H5) in (\lambda (H9: (eq T t t3)).(\lambda (_: (eq K k k0)).(let H11 \def (eq_ind_r T t4 (\lambda (t1: T).(or (eq T (THead k t t0) t1) ((eq T (THead k t t0) t1) \to (\forall (P: Prop).P)))) H2 t0 H8) in (let H12 \def (eq_ind_r T t3 (\lambda (t0: T).((eq T t t0) \to (\forall (P: Prop).P))) H4 t H9) in (let H13 \def (eq_ind_r T t3 (\lambda (t1: T).(or (eq T (THead k t t0) t1) ((eq T (THead k t t0) t1) \to (\forall (P: Prop).P)))) H1 t H9) in (H12 (refl_equal T t) P))))))) H7)) H6)))))) H3)))))))) t2))))))) t1).
  80
  81 theorem binder_dec:
  82  \forall (t: T).(or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t (THead (Bind b) w u)) \to (\forall (P: Prop).P))))))
  83 \def
  84  \lambda (t: T).(T_ind (\lambda (t0: T).(or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t0 (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t0 (THead (Bind b) w u)) \to (\forall (P: Prop).P))))))) (\lambda (n: nat).(or_intror (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T (TSort n) (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T (TSort n) (THead (Bind b) w u)) \to (\forall (P: Prop).P))))) (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(\lambda (H: (eq T (TSort n) (THead (Bind b) w u))).(\lambda (P: Prop).(let H0 \def (eq_ind T (TSort n) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) w u) H) in (False_ind P H0))))))))) (\lambda (n: nat).(or_intror (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T (TLRef n) (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T (TLRef n) (THead (Bind b) w u)) \to (\forall (P: Prop).P))))) (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(\lambda (H: (eq T (TLRef n) (THead (Bind b) w u))).(\lambda (P: Prop).(let H0 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) w u) H) in (False_ind P H0))))))))) (\lambda (k: K).(match k return (\lambda (k0: K).(\forall (t0: T).((or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t0 (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t0 (THead (Bind b) w u)) \to (\forall (P: Prop).P)))))) \to (\forall (t1: T).((or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t1 (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t1 (THead (Bind b) w u)) \to (\forall (P: Prop).P)))))) \to (or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T (THead k0 t0 t1) (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T (THead k0 t0 t1) (THead (Bind b) w u)) \to (\forall (P: Prop).P))))))))))) with [(Bind b) \Rightarrow (\lambda (t0: T).(\lambda (_: (or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t0 (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t0 (THead (Bind b) w u)) \to (\forall (P: Prop).P))))))).(\lambda (t1: T).(\lambda (_: (or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t1 (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t1 (THead (Bind b) w u)) \to (\forall (P: Prop).P))))))).(or_introl (ex_3 B T T (\lambda (b0: B).(\lambda (w: T).(\lambda (u: T).(eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u)))))) (\forall (b0: B).(\forall (w: T).(\forall (u: T).((eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u)) \to (\forall (P: Prop).P))))) (ex_3_intro B T T (\lambda (b0: B).(\lambda (w: T).(\lambda (u: T).(eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u))))) b t0 t1 (refl_equal T (THead (Bind b) t0 t1)))))))) | (Flat f) \Rightarrow (\lambda (t0: T).(\lambda (_: (or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t0 (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t0 (THead (Bind b) w u)) \to (\forall (P: Prop).P))))))).(\lambda (t1: T).(\lambda (_: (or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t1 (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t1 (THead (Bind b) w u)) \to (\forall (P: Prop).P))))))).(or_intror (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T (THead (Flat f) t0 t1) (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T (THead (Flat f) t0 t1) (THead (Bind b) w u)) \to (\forall (P: Prop).P))))) (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(\lambda (H1: (eq T (THead (Flat f) t0 t1) (THead (Bind b) w u))).(\lambda (P: Prop).(let H2 \def (eq_ind T (THead (Flat f) t0 t1) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) w u) H1) in (False_ind P H2))))))))))))])) t).
  85
  86 theorem abst_dec:
  87  \forall (u: T).(\forall (v: T).(or (ex T (\lambda (t: T).(eq T u (THead (Bind Abst) v t)))) (\forall (t: T).((eq T u (THead (Bind Abst) v t)) \to (\forall (P: Prop).P)))))
  88 \def
  89  \lambda (u: T).(match u return (\lambda (t: T).(\forall (v: T).(or (ex T (\lambda (t0: T).(eq T t (THead (Bind Abst) v t0)))) (\forall (t0: T).((eq T t (THead (Bind Abst) v t0)) \to (\forall (P: Prop).P)))))) with [(TSort n) \Rightarrow (\lambda (v: T).(or_intror (ex T (\lambda (t: T).(eq T (TSort n) (THead (Bind Abst) v t)))) (\forall (t: T).((eq T (TSort n) (THead (Bind Abst) v t)) \to (\forall (P: Prop).P))) (\lambda (t: T).(\lambda (H: (eq T (TSort n) (THead (Bind Abst) v t))).(\lambda (P: Prop).(let H0 \def (eq_ind T (TSort n) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) v t) H) in (False_ind P H0))))))) | (TLRef n) \Rightarrow (\lambda (v: T).(or_intror (ex T (\lambda (t: T).(eq T (TLRef n) (THead (Bind Abst) v t)))) (\forall (t: T).((eq T (TLRef n) (THead (Bind Abst) v t)) \to (\forall (P: Prop).P))) (\lambda (t: T).(\lambda (H: (eq T (TLRef n) (THead (Bind Abst) v t))).(\lambda (P: Prop).(let H0 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) v t) H) in (False_ind P H0))))))) | (THead k t t0) \Rightarrow (\lambda (v: T).(let H_x \def (terms_props__kind_dec k (Bind Abst)) in (let H \def H_x in (or_ind (eq K k (Bind Abst)) ((eq K k (Bind Abst)) \to (\forall (P: Prop).P)) (or (ex T (\lambda (t1: T).(eq T (THead k t t0) (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead k t t0) (THead (Bind Abst) v t1)) \to (\forall (P: Prop).P)))) (\lambda (H0: (eq K k (Bind Abst))).(eq_ind_r K (Bind Abst) (\lambda (k0: K).(or (ex T (\lambda (t1: T).(eq T (THead k0 t t0) (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead k0 t t0) (THead (Bind Abst) v t1)) \to (\forall (P: Prop).P))))) (let H_x0 \def (term_dec t v) in (let H1 \def H_x0 in (or_ind (eq T t v) ((eq T t v) \to (\forall (P: Prop).P)) (or (ex T (\lambda (t1: T).(eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)) \to (\forall (P: Prop).P)))) (\lambda (H2: (eq T t v)).(eq_ind T t (\lambda (t1: T).(or (ex T (\lambda (t2: T).(eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t1 t2)))) (\forall (t2: T).((eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t1 t2)) \to (\forall (P: Prop).P))))) (or_introl (ex T (\lambda (t1: T).(eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t1)))) (\forall (t1: T).((eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t1)) \to (\forall (P: Prop).P))) (ex_intro T (\lambda (t1: T).(eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t1))) t0 (refl_equal T (THead (Bind Abst) t t0)))) v H2)) (\lambda (H2: (((eq T t v) \to (\forall (P: Prop).P)))).(or_intror (ex T (\lambda (t1: T).(eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)) \to (\forall (P: Prop).P))) (\lambda (t1: T).(\lambda (H3: (eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1))).(\lambda (P: Prop).(let H4 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ t _) \Rightarrow t])) (THead (Bind Abst) t t0) (THead (Bind Abst) v t1) H3) in ((let H5 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead (Bind Abst) t t0) (THead (Bind Abst) v t1) H3) in (\lambda (H6: (eq T t v)).(H2 H6 P))) H4))))))) H1))) k H0)) (\lambda (H0: (((eq K k (Bind Abst)) \to (\forall (P: Prop).P)))).(or_intror (ex T (\lambda (t1: T).(eq T (THead k t t0) (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead k t t0) (THead (Bind Abst) v t1)) \to (\forall (P: Prop).P))) (\lambda (t1: T).(\lambda (H1: (eq T (THead k t t0) (THead (Bind Abst) v t1))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e: T).(match e return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k t t0) (THead (Bind Abst) v t1) H1) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ t _) \Rightarrow t])) (THead k t t0) (THead (Bind Abst) v t1) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k t t0) (THead (Bind Abst) v t1) H1) in (\lambda (_: (eq T t v)).(\lambda (H6: (eq K k (Bind Abst))).(H0 H6 P)))) H3)) H2))))))) H))))]).
  90
  91 theorem thead_x_y_y:
  92  \forall (k: K).(\forall (v: T).(\forall (t: T).((eq T (THead k v t) t) \to (\forall (P: Prop).P))))
  93 \def
  94  \lambda (k: K).(\lambda (v: T).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq T (THead k v t0) t0) \to (\forall (P: Prop).P))) (\lambda (n: nat).(\lambda (H: (eq T (THead k v (TSort n)) (TSort n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead k v (TSort n)) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H) in (False_ind P H0))))) (\lambda (n: nat).(\lambda (H: (eq T (THead k v (TLRef n)) (TLRef n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead k v (TLRef n)) (\lambda (ee: T).(match ee return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H) in (False_ind P H0))))) (\lambda (k0: K).(\lambda (t0: T).(\lambda (_: (((eq T (THead k v t0) t0) \to (\forall (P: Prop).P)))).(\lambda (t1: T).(\lambda (H0: (((eq T (THead k v t1) t1) \to (\forall (P: Prop).P)))).(\lambda (H1: (eq T (THead k v (THead k0 t0 t1)) (THead k0 t0 t1))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e: T).(match e return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t _) \Rightarrow t])) (THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e return (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead k0 t0 t1) | (TLRef _) \Rightarrow (THead k0 t0 t1) | (THead _ _ t) \Rightarrow t])) (THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) in (\lambda (H5: (eq T v t0)).(\lambda (H6: (eq K k k0)).(let H7 \def (eq_ind T v (\lambda (t: T).((eq T (THead k t t1) t1) \to (\forall (P: Prop).P))) H0 t0 H5) in (let H8 \def (eq_ind K k (\lambda (k: K).((eq T (THead k t0 t1) t1) \to (\forall (P: Prop).P))) H7 k0 H6) in (H8 H4 P)))))) H3)) H2))))))))) t))).
  95
  96 theorem s_S:
  97  \forall (k: K).(\forall (i: nat).(eq nat (s k (S i)) (S (s k i))))
  98 \def
  99  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(eq nat (s k0 (S i)) (S (s k0 i))))) (\lambda (b: B).(\lambda (i: nat).(refl_equal nat (S (s (Bind b) i))))) (\lambda (f: F).(\lambda (i: nat).(refl_equal nat (S (s (Flat f) i))))) k).
 100
 101 theorem s_plus:
 102  \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (s k (plus i j)) (plus (s k i) j))))
 103 \def
 104  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: nat).(eq nat (s k0 (plus i j)) (plus (s k0 i) j))))) (\lambda (b: B).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (plus (s (Bind b) i) j))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (plus (s (Flat f) i) j))))) k).
 105
 106 theorem s_plus_sym:
 107  \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (s k (plus i j)) (plus i (s k j)))))
 108 \def
 109  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: nat).(eq nat (s k0 (plus i j)) (plus i (s k0 j)))))) (\lambda (_: B).(\lambda (i: nat).(\lambda (j: nat).(eq_ind_r nat (plus i (S j)) (\lambda (n: nat).(eq nat n (plus i (S j)))) (refl_equal nat (plus i (S j))) (S (plus i j)) (plus_n_Sm i j))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (plus i (s (Flat f) j)))))) k).
 110
 111 theorem s_minus:
 112  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((le j i) \to (eq nat (s k (minus i j)) (minus (s k i) j)))))
 113 \def
 114  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: nat).((le j i) \to (eq nat (s k0 (minus i j)) (minus (s k0 i) j)))))) (\lambda (_: B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (le j i)).(eq_ind_r nat (minus (S i) j) (\lambda (n: nat).(eq nat n (minus (S i) j))) (refl_equal nat (minus (S i) j)) (S (minus i j)) (minus_Sn_m i j H)))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (_: (le j i)).(refl_equal nat (minus (s (Flat f) i) j)))))) k).
 115
 116 theorem minus_s_s:
 117  \forall (k: K).(\forall (i: nat).(\forall (j: nat).(eq nat (minus (s k i) (s k j)) (minus i j))))
 118 \def
 119  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: nat).(eq nat (minus (s k0 i) (s k0 j)) (minus i j))))) (\lambda (_: B).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (minus i j))))) (\lambda (_: F).(\lambda (i: nat).(\lambda (j: nat).(refl_equal nat (minus i j))))) k).
 120
 121 theorem s_le:
 122  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((le i j) \to (le (s k i) (s k j)))))
 123 \def
 124  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: nat).((le i j) \to (le (s k0 i) (s k0 j)))))) (\lambda (_: B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (le i j)).(le_S_n (S i) (S j) (lt_le_S (S i) (S (S j)) (lt_n_S i (S j) (le_lt_n_Sm i j H)))))))) (\lambda (_: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (le i j)).H)))) k).
 125
 126 theorem s_lt:
 127  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((lt i j) \to (lt (s k i) (s k j)))))
 128 \def
 129  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: nat).((lt i j) \to (lt (s k0 i) (s k0 j)))))) (\lambda (_: B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (lt i j)).(le_S_n (S (S i)) (S j) (le_n_S (S (S i)) (S j) (le_n_S (S i) j H))))))) (\lambda (_: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (lt i j)).H)))) k).
 130
 131 theorem s_inj:
 132  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((eq nat (s k i) (s k j)) \to (eq nat i j))))
 133 \def
 134  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: nat).((eq nat (s k0 i) (s k0 j)) \to (eq nat i j))))) (\lambda (b: B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (eq nat (s (Bind b) i) (s (Bind b) j))).(eq_add_S i j H))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (eq nat (s (Flat f) i) (s (Flat f) j))).H)))) k).
 135
 136 theorem s_arith0:
 137  \forall (k: K).(\forall (i: nat).(eq nat (minus (s k i) (s k O)) i))
 138 \def
 139  \lambda (k: K).(\lambda (i: nat).(eq_ind_r nat (minus i O) (\lambda (n: nat).(eq nat n i)) (eq_ind nat i (\lambda (n: nat).(eq nat n i)) (refl_equal nat i) (minus i O) (minus_n_O i)) (minus (s k i) (s k O)) (minus_s_s k i O))).
 140
 141 theorem s_arith1:
 142  \forall (b: B).(\forall (i: nat).(eq nat (minus (s (Bind b) i) (S O)) i))
 143 \def
 144  \lambda (_: B).(\lambda (i: nat).(eq_ind nat i (\lambda (n: nat).(eq nat n i)) (refl_equal nat i) (minus i O) (minus_n_O i))).
 145
 146 definition wadd:
 147  ((nat \to nat)) \to (nat \to (nat \to nat))
 148 \def
 149  \lambda (f: ((nat \to nat))).(\lambda (w: nat).(\lambda (n: nat).(match n with [O \Rightarrow w | (S m) \Rightarrow (f m)]))).
 150
 151 definition weight_map:
 152  ((nat \to nat)) \to (T \to nat)
 153 \def
 154  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.
 155
 156 definition weight:
 157  T \to nat
 158 \def
 159  weight_map (\lambda (_: nat).O).
 160
 161 definition tlt:
 162  T \to (T \to Prop)
 163 \def
 164  \lambda (t1: T).(\lambda (t2: T).(lt (weight t1) (weight t2))).
 165
 166 theorem wadd_le:
 167  \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))))))))
 168 \def
 169  \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))))))).
 170
 171 theorem wadd_lt:
 172  \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))))))))
 173 \def
 174  \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))))))).
 175
 176 theorem wadd_O:
 177  \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O)
 178 \def
 179  \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).
 180
 181 theorem weight_le:
 182  \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)))))
 183 \def
 184  \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).
 185
 186 theorem weight_eq:
 187  \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)))))
 188 \def
 189  \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)))))))).
 190
 191 theorem weight_add_O:
 192  \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t) (weight_map (\lambda (_: nat).O) t))
 193 \def
 194  \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_: nat).O) (\lambda (n: nat).(wadd_O n))).
 195
 196 theorem weight_add_S:
 197  \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O) O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
 198 \def
 199  \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)))))).
 200
 201 theorem tlt_trans:
 202  \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to (tlt u t)))))
 203 \def
 204  \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))))).
 205
 206 theorem tlt_head_sx:
 207  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
 208 \def
 209  \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).
 210
 211 theorem tlt_head_dx:
 212  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
 213 \def
 214  \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).
 215
 216 theorem tlt_wf__q_ind:
 217  \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)))
 218 \def
 219  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)))))).
 220
 221 theorem tlt_wf_ind:
 222  \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)))
 223 \def
 224  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)))).