matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/fwd.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 (* This file was automatically generated: do not edit *********************)
  16
  17 include "LambdaDelta-1/csubc/defs.ma".
  18
  19 theorem csubc_gen_sort_l:
  20  \forall (g: G).(\forall (x: C).(\forall (n: nat).((csubc g (CSort n) x) \to
  21 (eq C x (CSort n)))))
  22 \def
  23  \lambda (g: G).(\lambda (x: C).(\lambda (n: nat).(\lambda (H: (csubc g
  24 (CSort n) x)).(insert_eq C (CSort n) (\lambda (c: C).(csubc g c x)) (\lambda
  25 (c: C).(eq C x c)) (\lambda (y: C).(\lambda (H0: (csubc g y x)).(csubc_ind g
  26 (\lambda (c: C).(\lambda (c0: C).((eq C c (CSort n)) \to (eq C c0 c))))
  27 (\lambda (n0: nat).(\lambda (H1: (eq C (CSort n0) (CSort n))).(let H2 \def
  28 (f_equal C nat (\lambda (e: C).(match e in C return (\lambda (_: C).nat) with
  29 [(CSort n1) \Rightarrow n1 | (CHead _ _ _) \Rightarrow n0])) (CSort n0)
  30 (CSort n) H1) in (eq_ind_r nat n (\lambda (n1: nat).(eq C (CSort n1) (CSort
  31 n1))) (refl_equal C (CSort n)) n0 H2)))) (\lambda (c1: C).(\lambda (c2:
  32 C).(\lambda (_: (csubc g c1 c2)).(\lambda (_: (((eq C c1 (CSort n)) \to (eq C
  33 c2 c1)))).(\lambda (k: K).(\lambda (v: T).(\lambda (H3: (eq C (CHead c1 k v)
  34 (CSort n))).(let H4 \def (eq_ind C (CHead c1 k v) (\lambda (ee: C).(match ee
  35 in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead
  36 _ _ _) \Rightarrow True])) I (CSort n) H3) in (False_ind (eq C (CHead c2 k v)
  37 (CHead c1 k v)) H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_:
  38 (csubc g c1 c2)).(\lambda (_: (((eq C c1 (CSort n)) \to (eq C c2
  39 c1)))).(\lambda (v: T).(\lambda (a: A).(\lambda (_: (sc3 g (asucc g a) c1
  40 v)).(\lambda (w: T).(\lambda (_: (sc3 g a c2 w)).(\lambda (H5: (eq C (CHead
  41 c1 (Bind Abst) v) (CSort n))).(let H6 \def (eq_ind C (CHead c1 (Bind Abst) v)
  42 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
  43 \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H5) in
  44 (False_ind (eq C (CHead c2 (Bind Abbr) w) (CHead c1 (Bind Abst) v))
  45 H6)))))))))))) y x H0))) H)))).
  46
  47 theorem csubc_gen_head_l:
  48  \forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (k:
  49 K).((csubc g (CHead c1 k v) x) \to (or (ex2 C (\lambda (c2: C).(eq C x (CHead
  50 c2 k v))) (\lambda (c2: C).(csubc g c1 c2))) (ex5_3 C T A (\lambda (_:
  51 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c2:
  52 C).(\lambda (w: T).(\lambda (_: A).(eq C x (CHead c2 (Bind Abbr) w)))))
  53 (\lambda (c2: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c2)))) (\lambda
  54 (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda
  55 (c2: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c2 w)))))))))))
  56 \def
  57  \lambda (g: G).(\lambda (c1: C).(\lambda (x: C).(\lambda (v: T).(\lambda (k:
  58 K).(\lambda (H: (csubc g (CHead c1 k v) x)).(insert_eq C (CHead c1 k v)
  59 (\lambda (c: C).(csubc g c x)) (\lambda (_: C).(or (ex2 C (\lambda (c2:
  60 C).(eq C x (CHead c2 k v))) (\lambda (c2: C).(csubc g c1 c2))) (ex5_3 C T A
  61 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
  62 (\lambda (c2: C).(\lambda (w: T).(\lambda (_: A).(eq C x (CHead c2 (Bind
  63 Abbr) w))))) (\lambda (c2: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
  64 c2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1
  65 v)))) (\lambda (c2: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c2 w)))))))
  66 (\lambda (y: C).(\lambda (H0: (csubc g y x)).(csubc_ind g (\lambda (c:
  67 C).(\lambda (c0: C).((eq C c (CHead c1 k v)) \to (or (ex2 C (\lambda (c2:
  68 C).(eq C c0 (CHead c2 k v))) (\lambda (c2: C).(csubc g c1 c2))) (ex5_3 C T A
  69 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
  70 (\lambda (c2: C).(\lambda (w: T).(\lambda (_: A).(eq C c0 (CHead c2 (Bind
  71 Abbr) w))))) (\lambda (c2: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
  72 c2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1
  73 v)))) (\lambda (c2: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c2 w)))))))))
  74 (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead c1 k v))).(let H2 \def
  75 (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
  76 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
  77 False])) I (CHead c1 k v) H1) in (False_ind (or (ex2 C (\lambda (c2: C).(eq C
  78 (CSort n) (CHead c2 k v))) (\lambda (c2: C).(csubc g c1 c2))) (ex5_3 C T A
  79 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
  80 (\lambda (c2: C).(\lambda (w: T).(\lambda (_: A).(eq C (CSort n) (CHead c2
  81 (Bind Abbr) w))))) (\lambda (c2: C).(\lambda (_: T).(\lambda (_: A).(csubc g
  82 c1 c2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a)
  83 c1 v)))) (\lambda (c2: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c2 w))))))
  84 H2)))) (\lambda (c0: C).(\lambda (c2: C).(\lambda (H1: (csubc g c0
  85 c2)).(\lambda (H2: (((eq C c0 (CHead c1 k v)) \to (or (ex2 C (\lambda (c3:
  86 C).(eq C c2 (CHead c3 k v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A
  87 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
  88 (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind
  89 Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
  90 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1
  91 v)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3
  92 w))))))))).(\lambda (k0: K).(\lambda (v0: T).(\lambda (H3: (eq C (CHead c0 k0
  93 v0) (CHead c1 k v))).(let H4 \def (f_equal C C (\lambda (e: C).(match e in C
  94 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _)
  95 \Rightarrow c])) (CHead c0 k0 v0) (CHead c1 k v) H3) in ((let H5 \def
  96 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
  97 [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead c0 k0 v0)
  98 (CHead c1 k v) H3) in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in
  99 C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v0 | (CHead _ _ t)
 100 \Rightarrow t])) (CHead c0 k0 v0) (CHead c1 k v) H3) in (\lambda (H7: (eq K
 101 k0 k)).(\lambda (H8: (eq C c0 c1)).(eq_ind_r T v (\lambda (t: T).(or (ex2 C
 102 (\lambda (c3: C).(eq C (CHead c2 k0 t) (CHead c3 k v))) (\lambda (c3:
 103 C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
 104 (_: A).(eq K k (Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_:
 105 A).(eq C (CHead c2 k0 t) (CHead c3 (Bind Abbr) w))))) (\lambda (c3:
 106 C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda (_:
 107 C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda (c3:
 108 C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))))) (eq_ind_r K k
 109 (\lambda (k1: K).(or (ex2 C (\lambda (c3: C).(eq C (CHead c2 k1 v) (CHead c3
 110 k v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_:
 111 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c3:
 112 C).(\lambda (w: T).(\lambda (_: A).(eq C (CHead c2 k1 v) (CHead c3 (Bind
 113 Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
 114 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1
 115 v)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w)))))))
 116 (let H9 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c1 k v)) \to (or
 117 (ex2 C (\lambda (c3: C).(eq C c2 (CHead c3 k v))) (\lambda (c3: C).(csubc g
 118 c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k
 119 (Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C c2
 120 (CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
 121 A).(csubc g c1 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g
 122 (asucc g a) c1 v)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g
 123 a c3 w)))))))) H2 c1 H8) in (let H10 \def (eq_ind C c0 (\lambda (c: C).(csubc
 124 g c c2)) H1 c1 H8) in (or_introl (ex2 C (\lambda (c3: C).(eq C (CHead c2 k v)
 125 (CHead c3 k v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_:
 126 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c3:
 127 C).(\lambda (w: T).(\lambda (_: A).(eq C (CHead c2 k v) (CHead c3 (Bind Abbr)
 128 w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3))))
 129 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v))))
 130 (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w)))))
 131 (ex_intro2 C (\lambda (c3: C).(eq C (CHead c2 k v) (CHead c3 k v))) (\lambda
 132 (c3: C).(csubc g c1 c3)) c2 (refl_equal C (CHead c2 k v)) H10)))) k0 H7) v0
 133 H6)))) H5)) H4))))))))) (\lambda (c0: C).(\lambda (c2: C).(\lambda (H1:
 134 (csubc g c0 c2)).(\lambda (H2: (((eq C c0 (CHead c1 k v)) \to (or (ex2 C
 135 (\lambda (c3: C).(eq C c2 (CHead c3 k v))) (\lambda (c3: C).(csubc g c1 c3)))
 136 (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind
 137 Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C c2 (CHead c3
 138 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g
 139 c1 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a)
 140 c1 v)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3
 141 w))))))))).(\lambda (v0: T).(\lambda (a: A).(\lambda (H3: (sc3 g (asucc g a)
 142 c0 v0)).(\lambda (w: T).(\lambda (H4: (sc3 g a c2 w)).(\lambda (H5: (eq C
 143 (CHead c0 (Bind Abst) v0) (CHead c1 k v))).(let H6 \def (f_equal C C (\lambda
 144 (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0
 145 | (CHead c _ _) \Rightarrow c])) (CHead c0 (Bind Abst) v0) (CHead c1 k v) H5)
 146 in ((let H7 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda
 147 (_: C).K) with [(CSort _) \Rightarrow (Bind Abst) | (CHead _ k0 _)
 148 \Rightarrow k0])) (CHead c0 (Bind Abst) v0) (CHead c1 k v) H5) in ((let H8
 149 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
 150 with [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead c0
 151 (Bind Abst) v0) (CHead c1 k v) H5) in (\lambda (H9: (eq K (Bind Abst)
 152 k)).(\lambda (H10: (eq C c0 c1)).(let H11 \def (eq_ind T v0 (\lambda (t:
 153 T).(sc3 g (asucc g a) c0 t)) H3 v H8) in (let H12 \def (eq_ind C c0 (\lambda
 154 (c: C).(sc3 g (asucc g a) c v)) H11 c1 H10) in (let H13 \def (eq_ind C c0
 155 (\lambda (c: C).((eq C c (CHead c1 k v)) \to (or (ex2 C (\lambda (c3: C).(eq
 156 C c2 (CHead c3 k v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A
 157 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
 158 (\lambda (c3: C).(\lambda (w0: T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind
 159 Abbr) w0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
 160 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g (asucc g a0)
 161 c1 v)))) (\lambda (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3 g a0 c3
 162 w0)))))))) H2 c1 H10) in (let H14 \def (eq_ind C c0 (\lambda (c: C).(csubc g
 163 c c2)) H1 c1 H10) in (let H15 \def (eq_ind_r K k (\lambda (k0: K).((eq C c1
 164 (CHead c1 k0 v)) \to (or (ex2 C (\lambda (c3: C).(eq C c2 (CHead c3 k0 v)))
 165 (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
 166 T).(\lambda (_: A).(eq K k0 (Bind Abst))))) (\lambda (c3: C).(\lambda (w0:
 167 T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind Abbr) w0))))) (\lambda (c3:
 168 C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda (_:
 169 C).(\lambda (_: T).(\lambda (a0: A).(sc3 g (asucc g a0) c1 v)))) (\lambda
 170 (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3 g a0 c3 w0)))))))) H13 (Bind
 171 Abst) H9) in (eq_ind K (Bind Abst) (\lambda (k0: K).(or (ex2 C (\lambda (c3:
 172 C).(eq C (CHead c2 (Bind Abbr) w) (CHead c3 k0 v))) (\lambda (c3: C).(csubc g
 173 c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K
 174 k0 (Bind Abst))))) (\lambda (c3: C).(\lambda (w0: T).(\lambda (_: A).(eq C
 175 (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr) w0))))) (\lambda (c3:
 176 C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3)))) (\lambda (_:
 177 C).(\lambda (_: T).(\lambda (a0: A).(sc3 g (asucc g a0) c1 v)))) (\lambda
 178 (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3 g a0 c3 w0))))))) (or_intror
 179 (ex2 C (\lambda (c3: C).(eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abst)
 180 v))) (\lambda (c3: C).(csubc g c1 c3))) (ex5_3 C T A (\lambda (_: C).(\lambda
 181 (_: T).(\lambda (_: A).(eq K (Bind Abst) (Bind Abst))))) (\lambda (c3:
 182 C).(\lambda (w0: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) w) (CHead c3
 183 (Bind Abbr) w0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g
 184 c1 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g (asucc g
 185 a0) c1 v)))) (\lambda (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3 g a0 c3
 186 w0))))) (ex5_3_intro C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_:
 187 A).(eq K (Bind Abst) (Bind Abst))))) (\lambda (c3: C).(\lambda (w0:
 188 T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) w) (CHead c3 (Bind Abbr)
 189 w0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c3))))
 190 (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g (asucc g a0) c1 v))))
 191 (\lambda (c3: C).(\lambda (w0: T).(\lambda (a0: A).(sc3 g a0 c3 w0)))) c2 w a
 192 (refl_equal K (Bind Abst)) (refl_equal C (CHead c2 (Bind Abbr) w)) H14 H12
 193 H4)) k H9))))))))) H7)) H6)))))))))))) y x H0))) H)))))).
 194
 195 theorem csubc_gen_sort_r:
 196  \forall (g: G).(\forall (x: C).(\forall (n: nat).((csubc g x (CSort n)) \to
 197 (eq C x (CSort n)))))
 198 \def
 199  \lambda (g: G).(\lambda (x: C).(\lambda (n: nat).(\lambda (H: (csubc g x
 200 (CSort n))).(insert_eq C (CSort n) (\lambda (c: C).(csubc g x c)) (\lambda
 201 (c: C).(eq C x c)) (\lambda (y: C).(\lambda (H0: (csubc g x y)).(csubc_ind g
 202 (\lambda (c: C).(\lambda (c0: C).((eq C c0 (CSort n)) \to (eq C c c0))))
 203 (\lambda (n0: nat).(\lambda (H1: (eq C (CSort n0) (CSort n))).(let H2 \def
 204 (f_equal C nat (\lambda (e: C).(match e in C return (\lambda (_: C).nat) with
 205 [(CSort n1) \Rightarrow n1 | (CHead _ _ _) \Rightarrow n0])) (CSort n0)
 206 (CSort n) H1) in (eq_ind_r nat n (\lambda (n1: nat).(eq C (CSort n1) (CSort
 207 n1))) (refl_equal C (CSort n)) n0 H2)))) (\lambda (c1: C).(\lambda (c2:
 208 C).(\lambda (_: (csubc g c1 c2)).(\lambda (_: (((eq C c2 (CSort n)) \to (eq C
 209 c1 c2)))).(\lambda (k: K).(\lambda (v: T).(\lambda (H3: (eq C (CHead c2 k v)
 210 (CSort n))).(let H4 \def (eq_ind C (CHead c2 k v) (\lambda (ee: C).(match ee
 211 in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead
 212 _ _ _) \Rightarrow True])) I (CSort n) H3) in (False_ind (eq C (CHead c1 k v)
 213 (CHead c2 k v)) H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_:
 214 (csubc g c1 c2)).(\lambda (_: (((eq C c2 (CSort n)) \to (eq C c1
 215 c2)))).(\lambda (v: T).(\lambda (a: A).(\lambda (_: (sc3 g (asucc g a) c1
 216 v)).(\lambda (w: T).(\lambda (_: (sc3 g a c2 w)).(\lambda (H5: (eq C (CHead
 217 c2 (Bind Abbr) w) (CSort n))).(let H6 \def (eq_ind C (CHead c2 (Bind Abbr) w)
 218 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
 219 \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H5) in
 220 (False_ind (eq C (CHead c1 (Bind Abst) v) (CHead c2 (Bind Abbr) w))
 221 H6)))))))))))) x y H0))) H)))).
 222
 223 theorem csubc_gen_head_r:
 224  \forall (g: G).(\forall (c2: C).(\forall (x: C).(\forall (w: T).(\forall (k:
 225 K).((csubc g x (CHead c2 k w)) \to (or (ex2 C (\lambda (c1: C).(eq C x (CHead
 226 c1 k w))) (\lambda (c1: C).(csubc g c1 c2))) (ex5_3 C T A (\lambda (_:
 227 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c1:
 228 C).(\lambda (v: T).(\lambda (_: A).(eq C x (CHead c1 (Bind Abst) v)))))
 229 (\lambda (c1: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 c2)))) (\lambda
 230 (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda
 231 (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w)))))))))))
 232 \def
 233  \lambda (g: G).(\lambda (c2: C).(\lambda (x: C).(\lambda (w: T).(\lambda (k:
 234 K).(\lambda (H: (csubc g x (CHead c2 k w))).(insert_eq C (CHead c2 k w)
 235 (\lambda (c: C).(csubc g x c)) (\lambda (_: C).(or (ex2 C (\lambda (c1:
 236 C).(eq C x (CHead c1 k w))) (\lambda (c1: C).(csubc g c1 c2))) (ex5_3 C T A
 237 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr)))))
 238 (\lambda (c1: C).(\lambda (v: T).(\lambda (_: A).(eq C x (CHead c1 (Bind
 239 Abst) v))))) (\lambda (c1: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
 240 c2)))) (\lambda (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c1
 241 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w)))))))
 242 (\lambda (y: C).(\lambda (H0: (csubc g x y)).(csubc_ind g (\lambda (c:
 243 C).(\lambda (c0: C).((eq C c0 (CHead c2 k w)) \to (or (ex2 C (\lambda (c1:
 244 C).(eq C c (CHead c1 k w))) (\lambda (c1: C).(csubc g c1 c2))) (ex5_3 C T A
 245 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr)))))
 246 (\lambda (c1: C).(\lambda (v: T).(\lambda (_: A).(eq C c (CHead c1 (Bind
 247 Abst) v))))) (\lambda (c1: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
 248 c2)))) (\lambda (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c1
 249 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w)))))))))
 250 (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead c2 k w))).(let H2 \def
 251 (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
 252 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
 253 False])) I (CHead c2 k w) H1) in (False_ind (or (ex2 C (\lambda (c1: C).(eq C
 254 (CSort n) (CHead c1 k w))) (\lambda (c1: C).(csubc g c1 c2))) (ex5_3 C T A
 255 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr)))))
 256 (\lambda (c1: C).(\lambda (v: T).(\lambda (_: A).(eq C (CSort n) (CHead c1
 257 (Bind Abst) v))))) (\lambda (c1: C).(\lambda (_: T).(\lambda (_: A).(csubc g
 258 c1 c2)))) (\lambda (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a)
 259 c1 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))))
 260 H2)))) (\lambda (c1: C).(\lambda (c0: C).(\lambda (H1: (csubc g c1
 261 c0)).(\lambda (H2: (((eq C c0 (CHead c2 k w)) \to (or (ex2 C (\lambda (c3:
 262 C).(eq C c1 (CHead c3 k w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A
 263 (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr)))))
 264 (\lambda (c3: C).(\lambda (v: T).(\lambda (_: A).(eq C c1 (CHead c3 (Bind
 265 Abst) v))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3
 266 c2)))) (\lambda (c3: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c3
 267 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2
 268 w))))))))).(\lambda (k0: K).(\lambda (v: T).(\lambda (H3: (eq C (CHead c0 k0
 269 v) (CHead c2 k w))).(let H4 \def (f_equal C C (\lambda (e: C).(match e in C
 270 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _)
 271 \Rightarrow c])) (CHead c0 k0 v) (CHead c2 k w) H3) in ((let H5 \def (f_equal
 272 C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with [(CSort _)
 273 \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead c0 k0 v) (CHead c2 k
 274 w) H3) in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return
 275 (\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t) \Rightarrow
 276 t])) (CHead c0 k0 v) (CHead c2 k w) H3) in (\lambda (H7: (eq K k0
 277 k)).(\lambda (H8: (eq C c0 c2)).(eq_ind_r T w (\lambda (t: T).(or (ex2 C
 278 (\lambda (c3: C).(eq C (CHead c1 k0 t) (CHead c3 k w))) (\lambda (c3:
 279 C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
 280 (_: A).(eq K k (Bind Abbr))))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (_:
 281 A).(eq C (CHead c1 k0 t) (CHead c3 (Bind Abst) v0))))) (\lambda (c3:
 282 C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3:
 283 C).(\lambda (v0: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v0)))) (\lambda (_:
 284 C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))))) (eq_ind_r K k
 285 (\lambda (k1: K).(or (ex2 C (\lambda (c3: C).(eq C (CHead c1 k1 w) (CHead c3
 286 k w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_:
 287 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c3:
 288 C).(\lambda (v0: T).(\lambda (_: A).(eq C (CHead c1 k1 w) (CHead c3 (Bind
 289 Abst) v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3
 290 c2)))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (a: A).(sc3 g (asucc g a)
 291 c3 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2
 292 w))))))) (let H9 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c2 k w))
 293 \to (or (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k w))) (\lambda (c3:
 294 C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
 295 (_: A).(eq K k (Bind Abbr))))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (_:
 296 A).(eq C c1 (CHead c3 (Bind Abst) v0))))) (\lambda (c3: C).(\lambda (_:
 297 T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v0:
 298 T).(\lambda (a: A).(sc3 g (asucc g a) c3 v0)))) (\lambda (_: C).(\lambda (_:
 299 T).(\lambda (a: A).(sc3 g a c2 w)))))))) H2 c2 H8) in (let H10 \def (eq_ind C
 300 c0 (\lambda (c: C).(csubc g c1 c)) H1 c2 H8) in (or_introl (ex2 C (\lambda
 301 (c3: C).(eq C (CHead c1 k w) (CHead c3 k w))) (\lambda (c3: C).(csubc g c3
 302 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k
 303 (Bind Abbr))))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (_: A).(eq C
 304 (CHead c1 k w) (CHead c3 (Bind Abst) v0))))) (\lambda (c3: C).(\lambda (_:
 305 T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v0:
 306 T).(\lambda (a: A).(sc3 g (asucc g a) c3 v0)))) (\lambda (_: C).(\lambda (_:
 307 T).(\lambda (a: A).(sc3 g a c2 w))))) (ex_intro2 C (\lambda (c3: C).(eq C
 308 (CHead c1 k w) (CHead c3 k w))) (\lambda (c3: C).(csubc g c3 c2)) c1
 309 (refl_equal C (CHead c1 k w)) H10)))) k0 H7) v H6)))) H5)) H4)))))))))
 310 (\lambda (c1: C).(\lambda (c0: C).(\lambda (H1: (csubc g c1 c0)).(\lambda
 311 (H2: (((eq C c0 (CHead c2 k w)) \to (or (ex2 C (\lambda (c3: C).(eq C c1
 312 (CHead c3 k w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_:
 313 C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c3:
 314 C).(\lambda (v: T).(\lambda (_: A).(eq C c1 (CHead c3 (Bind Abst) v)))))
 315 (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda
 316 (c3: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c3 v)))) (\lambda
 317 (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a c2 w))))))))).(\lambda (v:
 318 T).(\lambda (a: A).(\lambda (H3: (sc3 g (asucc g a) c1 v)).(\lambda (w0:
 319 T).(\lambda (H4: (sc3 g a c0 w0)).(\lambda (H5: (eq C (CHead c0 (Bind Abbr)
 320 w0) (CHead c2 k w))).(let H6 \def (f_equal C C (\lambda (e: C).(match e in C
 321 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _)
 322 \Rightarrow c])) (CHead c0 (Bind Abbr) w0) (CHead c2 k w) H5) in ((let H7
 323 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
 324 with [(CSort _) \Rightarrow (Bind Abbr) | (CHead _ k0 _) \Rightarrow k0]))
 325 (CHead c0 (Bind Abbr) w0) (CHead c2 k w) H5) in ((let H8 \def (f_equal C T
 326 (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
 327 \Rightarrow w0 | (CHead _ _ t) \Rightarrow t])) (CHead c0 (Bind Abbr) w0)
 328 (CHead c2 k w) H5) in (\lambda (H9: (eq K (Bind Abbr) k)).(\lambda (H10: (eq
 329 C c0 c2)).(let H11 \def (eq_ind T w0 (\lambda (t: T).(sc3 g a c0 t)) H4 w H8)
 330 in (let H12 \def (eq_ind C c0 (\lambda (c: C).(sc3 g a c w)) H11 c2 H10) in
 331 (let H13 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c2 k w)) \to (or
 332 (ex2 C (\lambda (c3: C).(eq C c1 (CHead c3 k w))) (\lambda (c3: C).(csubc g
 333 c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k
 334 (Bind Abbr))))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (_: A).(eq C c1
 335 (CHead c3 (Bind Abst) v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
 336 A).(csubc g c3 c2)))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (a0: A).(sc3
 337 g (asucc g a0) c3 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0:
 338 A).(sc3 g a0 c2 w)))))))) H2 c2 H10) in (let H14 \def (eq_ind C c0 (\lambda
 339 (c: C).(csubc g c1 c)) H1 c2 H10) in (let H15 \def (eq_ind_r K k (\lambda
 340 (k0: K).((eq C c2 (CHead c2 k0 w)) \to (or (ex2 C (\lambda (c3: C).(eq C c1
 341 (CHead c3 k0 w))) (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda
 342 (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k0 (Bind Abbr))))) (\lambda (c3:
 343 C).(\lambda (v0: T).(\lambda (_: A).(eq C c1 (CHead c3 (Bind Abst) v0)))))
 344 (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda
 345 (c3: C).(\lambda (v0: T).(\lambda (a0: A).(sc3 g (asucc g a0) c3 v0))))
 346 (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g a0 c2 w)))))))) H13
 347 (Bind Abbr) H9) in (eq_ind K (Bind Abbr) (\lambda (k0: K).(or (ex2 C (\lambda
 348 (c3: C).(eq C (CHead c1 (Bind Abst) v) (CHead c3 k0 w))) (\lambda (c3:
 349 C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda
 350 (_: A).(eq K k0 (Bind Abbr))))) (\lambda (c3: C).(\lambda (v0: T).(\lambda
 351 (_: A).(eq C (CHead c1 (Bind Abst) v) (CHead c3 (Bind Abst) v0))))) (\lambda
 352 (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3:
 353 C).(\lambda (v0: T).(\lambda (a0: A).(sc3 g (asucc g a0) c3 v0)))) (\lambda
 354 (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g a0 c2 w))))))) (or_intror (ex2
 355 C (\lambda (c3: C).(eq C (CHead c1 (Bind Abst) v) (CHead c3 (Bind Abbr) w)))
 356 (\lambda (c3: C).(csubc g c3 c2))) (ex5_3 C T A (\lambda (_: C).(\lambda (_:
 357 T).(\lambda (_: A).(eq K (Bind Abbr) (Bind Abbr))))) (\lambda (c3:
 358 C).(\lambda (v0: T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) v) (CHead c3
 359 (Bind Abst) v0))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g
 360 c3 c2)))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (a0: A).(sc3 g (asucc g
 361 a0) c3 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g a0 c2
 362 w))))) (ex5_3_intro C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq
 363 K (Bind Abbr) (Bind Abbr))))) (\lambda (c3: C).(\lambda (v0: T).(\lambda (_:
 364 A).(eq C (CHead c1 (Bind Abst) v) (CHead c3 (Bind Abst) v0))))) (\lambda (c3:
 365 C).(\lambda (_: T).(\lambda (_: A).(csubc g c3 c2)))) (\lambda (c3:
 366 C).(\lambda (v0: T).(\lambda (a0: A).(sc3 g (asucc g a0) c3 v0)))) (\lambda
 367 (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g a0 c2 w)))) c1 v a (refl_equal
 368 K (Bind Abbr)) (refl_equal C (CHead c1 (Bind Abst) v)) H14 H3 H12)) k
 369 H9))))))))) H7)) H6)))))))))))) x y H0))) H)))))).
 370