matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/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/csuba/defs.ma".
  18
  19 theorem csuba_gen_abbr:
  20  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g
  21 (CHead d1 (Bind Abbr) u) c) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
  22 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))))
  23 \def
  24  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
  25 (csuba g (CHead d1 (Bind Abbr) u) c)).(insert_eq C (CHead d1 (Bind Abbr) u)
  26 (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(ex2 C (\lambda (d2: C).(eq
  27 C c (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (\lambda
  28 (y: C).(\lambda (H0: (csuba g y c)).(csuba_ind g (\lambda (c0: C).(\lambda
  29 (c1: C).((eq C c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(eq C
  30 c1 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda
  31 (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abbr) u))).(let H2
  32 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
  33 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
  34 False])) I (CHead d1 (Bind Abbr) u) H1) in (False_ind (ex2 C (\lambda (d2:
  35 C).(eq C (CSort n) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
  36 d2))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
  37 c2)).(\lambda (H2: (((eq C c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda
  38 (d2: C).(eq C c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
  39 d2)))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c1 k u0)
  40 (CHead d1 (Bind Abbr) u))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
  41 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _
  42 _) \Rightarrow c0])) (CHead c1 k u0) (CHead d1 (Bind Abbr) u) H3) in ((let H5
  43 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
  44 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k
  45 u0) (CHead d1 (Bind Abbr) u) H3) in ((let H6 \def (f_equal C T (\lambda (e:
  46 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
  47 (CHead _ _ t) \Rightarrow t])) (CHead c1 k u0) (CHead d1 (Bind Abbr) u) H3)
  48 in (\lambda (H7: (eq K k (Bind Abbr))).(\lambda (H8: (eq C c1 d1)).(eq_ind_r
  49 T u (\lambda (t: T).(ex2 C (\lambda (d2: C).(eq C (CHead c2 k t) (CHead d2
  50 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (eq_ind_r K (Bind Abbr)
  51 (\lambda (k0: K).(ex2 C (\lambda (d2: C).(eq C (CHead c2 k0 u) (CHead d2
  52 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H9 \def (eq_ind C
  53 c1 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda
  54 (d2: C).(eq C c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
  55 d2))))) H2 d1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0
  56 c2)) H1 d1 H8) in (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr)
  57 u) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) c2
  58 (refl_equal C (CHead c2 (Bind Abbr) u)) H10))) k H7) u0 H6)))) H5))
  59 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
  60 c2)).(\lambda (_: (((eq C c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda
  61 (d2: C).(eq C c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
  62 d2)))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
  63 a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
  64 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abbr) u))).(let H6 \def (eq_ind C
  65 (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match ee in C return (\lambda (_:
  66 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
  67 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
  68 return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow
  69 True | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead d1
  70 (Bind Abbr) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c2
  71 (Bind Abbr) u0) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))
  72 H6)))))))))))) y c H0))) H))))).
  73
  74 theorem csuba_gen_void:
  75  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g
  76 (CHead d1 (Bind Void) u) c) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
  77 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))))))
  78 \def
  79  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
  80 (csuba g (CHead d1 (Bind Void) u) c)).(insert_eq C (CHead d1 (Bind Void) u)
  81 (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(ex2 C (\lambda (d2: C).(eq
  82 C c (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))) (\lambda
  83 (y: C).(\lambda (H0: (csuba g y c)).(csuba_ind g (\lambda (c0: C).(\lambda
  84 (c1: C).((eq C c0 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C
  85 c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda
  86 (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Void) u))).(let H2
  87 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
  88 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
  89 False])) I (CHead d1 (Bind Void) u) H1) in (False_ind (ex2 C (\lambda (d2:
  90 C).(eq C (CSort n) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1
  91 d2))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
  92 c2)).(\lambda (H2: (((eq C c1 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
  93 (d2: C).(eq C c2 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1
  94 d2)))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c1 k u0)
  95 (CHead d1 (Bind Void) u))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
  96 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _
  97 _) \Rightarrow c0])) (CHead c1 k u0) (CHead d1 (Bind Void) u) H3) in ((let H5
  98 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
  99 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k
 100 u0) (CHead d1 (Bind Void) u) H3) in ((let H6 \def (f_equal C T (\lambda (e:
 101 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
 102 (CHead _ _ t) \Rightarrow t])) (CHead c1 k u0) (CHead d1 (Bind Void) u) H3)
 103 in (\lambda (H7: (eq K k (Bind Void))).(\lambda (H8: (eq C c1 d1)).(eq_ind_r
 104 T u (\lambda (t: T).(ex2 C (\lambda (d2: C).(eq C (CHead c2 k t) (CHead d2
 105 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))) (eq_ind_r K (Bind Void)
 106 (\lambda (k0: K).(ex2 C (\lambda (d2: C).(eq C (CHead c2 k0 u) (CHead d2
 107 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H9 \def (eq_ind C
 108 c1 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
 109 (d2: C).(eq C c2 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1
 110 d2))))) H2 d1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0
 111 c2)) H1 d1 H8) in (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Void)
 112 u) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)) c2
 113 (refl_equal C (CHead c2 (Bind Void) u)) H10))) k H7) u0 H6)))) H5))
 114 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
 115 c2)).(\lambda (_: (((eq C c1 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
 116 (d2: C).(eq C c2 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1
 117 d2)))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
 118 a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
 119 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Void) u))).(let H6 \def (eq_ind C
 120 (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match ee in C return (\lambda (_:
 121 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
 122 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
 123 return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow
 124 True | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead d1
 125 (Bind Void) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c2
 126 (Bind Abbr) u0) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))
 127 H6)))))))))))) y c H0))) H))))).
 128
 129 theorem csuba_gen_abst:
 130  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g
 131 (CHead d1 (Bind Abst) u1) c) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead
 132 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
 133 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr)
 134 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
 135 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
 136 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
 137 a))))))))))
 138 \def
 139  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
 140 (H: (csuba g (CHead d1 (Bind Abst) u1) c)).(insert_eq C (CHead d1 (Bind Abst)
 141 u1) (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(or (ex2 C (\lambda (d2:
 142 C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
 143 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead
 144 d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 145 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
 146 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
 147 A).(arity g d2 u2 a))))))) (\lambda (y: C).(\lambda (H0: (csuba g y
 148 c)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c0 (CHead d1 (Bind
 149 Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead d2 (Bind Abst)
 150 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
 151 C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abbr) u2)))))
 152 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
 153 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
 154 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))))
 155 (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abst)
 156 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
 157 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
 158 \Rightarrow False])) I (CHead d1 (Bind Abst) u1) H1) in (False_ind (or (ex2 C
 159 (\lambda (d2: C).(eq C (CSort n) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
 160 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
 161 (_: A).(eq C (CSort n) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
 162 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
 163 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
 164 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) H2))))
 165 (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda
 166 (H2: (((eq C c1 (CHead d1 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2:
 167 C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
 168 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2
 169 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 170 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
 171 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
 172 A).(arity g d2 u2 a))))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3:
 173 (eq C (CHead c1 k u) (CHead d1 (Bind Abst) u1))).(let H4 \def (f_equal C C
 174 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
 175 \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 k u) (CHead d1
 176 (Bind Abst) u1) H3) in ((let H5 \def (f_equal C K (\lambda (e: C).(match e in
 177 C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _)
 178 \Rightarrow k0])) (CHead c1 k u) (CHead d1 (Bind Abst) u1) H3) in ((let H6
 179 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
 180 with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c1 k u)
 181 (CHead d1 (Bind Abst) u1) H3) in (\lambda (H7: (eq K k (Bind Abst))).(\lambda
 182 (H8: (eq C c1 d1)).(eq_ind_r T u1 (\lambda (t: T).(or (ex2 C (\lambda (d2:
 183 C).(eq C (CHead c2 k t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
 184 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C
 185 (CHead c2 k t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
 186 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
 187 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
 188 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))) (eq_ind_r K (Bind Abst)
 189 (\lambda (k0: K).(or (ex2 C (\lambda (d2: C).(eq C (CHead c2 k0 u1) (CHead d2
 190 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
 191 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 k0 u1) (CHead d2
 192 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
 193 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
 194 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
 195 u2 a))))))) (let H9 \def (eq_ind C c1 (\lambda (c0: C).((eq C c0 (CHead d1
 196 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
 197 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
 198 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
 199 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
 200 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
 201 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))) H2
 202 d1 H8) in (let H10 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0 c2)) H1 d1
 203 H8) in (or_introl (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1)
 204 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
 205 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abst)
 206 u1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
 207 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
 208 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
 209 (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2
 210 (Bind Abst) u1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))
 211 c2 (refl_equal C (CHead c2 (Bind Abst) u1)) H10)))) k H7) u H6)))) H5))
 212 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
 213 c2)).(\lambda (H2: (((eq C c1 (CHead d1 (Bind Abst) u1)) \to (or (ex2 C
 214 (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
 215 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
 216 C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
 217 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
 218 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
 219 (a: A).(arity g d2 u2 a))))))))).(\lambda (t: T).(\lambda (a: A).(\lambda
 220 (H3: (arity g c1 t (asucc g a))).(\lambda (u: T).(\lambda (H4: (arity g c2 u
 221 a)).(\lambda (H5: (eq C (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst)
 222 u1))).(let H6 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
 223 (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0]))
 224 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst) u1) H5) in ((let H7 \def
 225 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
 226 [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (CHead c1 (Bind
 227 Abst) t) (CHead d1 (Bind Abst) u1) H5) in (\lambda (H8: (eq C c1 d1)).(let H9
 228 \def (eq_ind T t (\lambda (t0: T).(arity g c1 t0 (asucc g a))) H3 u1 H7) in
 229 (let H10 \def (eq_ind C c1 (\lambda (c0: C).(arity g c0 u1 (asucc g a))) H9
 230 d1 H8) in (let H11 \def (eq_ind C c1 (\lambda (c0: C).((eq C c0 (CHead d1
 231 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
 232 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
 233 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
 234 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
 235 (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g a0)))))
 236 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 a0))))))))
 237 H2 d1 H8) in (let H12 \def (eq_ind C c1 (\lambda (c0: C).(csuba g c0 c2)) H1
 238 d1 H8) in (or_intror (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u)
 239 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
 240 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr)
 241 u) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
 242 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0:
 243 A).(arity g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
 244 (a0: A).(arity g d2 u2 a0))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda
 245 (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abbr)
 246 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
 247 (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g
 248 a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2
 249 a0)))) c2 u a (refl_equal C (CHead c2 (Bind Abbr) u)) H12 H10 H4))))))))
 250 H6)))))))))))) y c H0))) H))))).
 251
 252 theorem csuba_gen_flat:
 253  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
 254 (f: F).((csuba g (CHead d1 (Flat f) u1) c) \to (ex2_2 C T (\lambda (d2:
 255 C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2:
 256 C).(\lambda (_: T).(csuba g d1 d2)))))))))
 257 \def
 258  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
 259 (f: F).(\lambda (H: (csuba g (CHead d1 (Flat f) u1) c)).(insert_eq C (CHead
 260 d1 (Flat f) u1) (\lambda (c0: C).(csuba g c0 c)) (\lambda (_: C).(ex2_2 C T
 261 (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda
 262 (d2: C).(\lambda (_: T).(csuba g d1 d2))))) (\lambda (y: C).(\lambda (H0:
 263 (csuba g y c)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c0
 264 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
 265 C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
 266 d2))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Flat f)
 267 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
 268 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
 269 \Rightarrow False])) I (CHead d1 (Flat f) u1) H1) in (False_ind (ex2_2 C T
 270 (\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead d2 (Flat f) u2))))
 271 (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))) H2)))) (\lambda (c1:
 272 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c1
 273 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
 274 C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
 275 d2))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c1 k u)
 276 (CHead d1 (Flat f) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
 277 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _
 278 _) \Rightarrow c0])) (CHead c1 k u) (CHead d1 (Flat f) u1) H3) in ((let H5
 279 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
 280 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k
 281 u) (CHead d1 (Flat f) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
 282 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
 283 (CHead _ _ t) \Rightarrow t])) (CHead c1 k u) (CHead d1 (Flat f) u1) H3) in
 284 (\lambda (H7: (eq K k (Flat f))).(\lambda (H8: (eq C c1 d1)).(eq_ind_r T u1
 285 (\lambda (t: T).(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2
 286 k t) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
 287 d2))))) (eq_ind_r K (Flat f) (\lambda (k0: K).(ex2_2 C T (\lambda (d2:
 288 C).(\lambda (u2: T).(eq C (CHead c2 k0 u1) (CHead d2 (Flat f) u2)))) (\lambda
 289 (d2: C).(\lambda (_: T).(csuba g d1 d2))))) (let H9 \def (eq_ind C c1
 290 (\lambda (c0: C).((eq C c0 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda
 291 (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2:
 292 C).(\lambda (_: T).(csuba g d1 d2)))))) H2 d1 H8) in (let H10 \def (eq_ind C
 293 c1 (\lambda (c0: C).(csuba g c0 c2)) H1 d1 H8) in (ex2_2_intro C T (\lambda
 294 (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Flat f) u1) (CHead d2 (Flat f)
 295 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))) c2 u1 (refl_equal C
 296 (CHead c2 (Flat f) u1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
 297 C).(\lambda (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c1
 298 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
 299 C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
 300 d2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
 301 a))).(\lambda (u: T).(\lambda (_: (arity g c2 u a)).(\lambda (H5: (eq C
 302 (CHead c1 (Bind Abst) t) (CHead d1 (Flat f) u1))).(let H6 \def (eq_ind C
 303 (CHead c1 (Bind Abst) t) (\lambda (ee: C).(match ee in C return (\lambda (_:
 304 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
 305 k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat
 306 _) \Rightarrow False])])) I (CHead d1 (Flat f) u1) H5) in (False_ind (ex2_2 C
 307 T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Bind Abbr) u) (CHead d2
 308 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))))
 309 H6)))))))))))) y c H0))) H)))))).
 310
 311 theorem csuba_gen_bind:
 312  \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
 313 (v1: T).((csuba g (CHead e1 (Bind b1) v1) c2) \to (ex2_3 B C T (\lambda (b2:
 314 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
 315 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))))))
 316 \def
 317  \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
 318 (v1: T).(\lambda (H: (csuba g (CHead e1 (Bind b1) v1) c2)).(insert_eq C
 319 (CHead e1 (Bind b1) v1) (\lambda (c: C).(csuba g c c2)) (\lambda (_:
 320 C).(ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
 321 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 322 T).(csuba g e1 e2)))))) (\lambda (y: C).(\lambda (H0: (csuba g y
 323 c2)).(csuba_ind g (\lambda (c: C).(\lambda (c0: C).((eq C c (CHead e1 (Bind
 324 b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
 325 T).(eq C c0 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
 326 C).(\lambda (_: T).(csuba g e1 e2)))))))) (\lambda (n: nat).(\lambda (H1: (eq
 327 C (CSort n) (CHead e1 (Bind b1) v1))).(let H2 \def (eq_ind C (CSort n)
 328 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
 329 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind b1)
 330 v1) H1) in (False_ind (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
 331 (v2: T).(eq C (CSort n) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
 332 (e2: C).(\lambda (_: T).(csuba g e1 e2))))) H2)))) (\lambda (c1: C).(\lambda
 333 (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c1 (CHead e1
 334 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
 335 (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
 336 C).(\lambda (_: T).(csuba g e1 e2)))))))).(\lambda (k: K).(\lambda (u:
 337 T).(\lambda (H3: (eq C (CHead c1 k u) (CHead e1 (Bind b1) v1))).(let H4 \def
 338 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
 339 [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 k u)
 340 (CHead e1 (Bind b1) v1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
 341 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
 342 (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H3)
 343 in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
 344 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
 345 (CHead c1 k u) (CHead e1 (Bind b1) v1) H3) in (\lambda (H7: (eq K k (Bind
 346 b1))).(\lambda (H8: (eq C c1 e1)).(eq_ind_r T v1 (\lambda (t: T).(ex2_3 B C T
 347 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 k t)
 348 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 349 T).(csuba g e1 e2)))))) (eq_ind_r K (Bind b1) (\lambda (k0: K).(ex2_3 B C T
 350 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 k0 v1)
 351 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 352 T).(csuba g e1 e2)))))) (let H9 \def (eq_ind C c1 (\lambda (c: C).((eq C c
 353 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
 354 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
 355 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))) H2 e1 H8) in (let
 356 H10 \def (eq_ind C c1 (\lambda (c: C).(csuba g c c3)) H1 e1 H8) in
 357 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
 358 (CHead c3 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
 359 (e2: C).(\lambda (_: T).(csuba g e1 e2)))) b1 c3 v1 (refl_equal C (CHead c3
 360 (Bind b1) v1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
 361 C).(\lambda (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c1
 362 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
 363 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
 364 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2)))))))).(\lambda (t:
 365 T).(\lambda (a: A).(\lambda (H3: (arity g c1 t (asucc g a))).(\lambda (u:
 366 T).(\lambda (_: (arity g c3 u a)).(\lambda (H5: (eq C (CHead c1 (Bind Abst)
 367 t) (CHead e1 (Bind b1) v1))).(let H6 \def (f_equal C C (\lambda (e: C).(match
 368 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c _
 369 _) \Rightarrow c])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H5) in
 370 ((let H7 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
 371 C).B) with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k
 372 in K return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _)
 373 \Rightarrow Abst])])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H5) in
 374 ((let H8 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
 375 C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (CHead
 376 c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H5) in (\lambda (H9: (eq B Abst
 377 b1)).(\lambda (H10: (eq C c1 e1)).(let H11 \def (eq_ind T t (\lambda (t0:
 378 T).(arity g c1 t0 (asucc g a))) H3 v1 H8) in (let H12 \def (eq_ind C c1
 379 (\lambda (c: C).(arity g c v1 (asucc g a))) H11 e1 H10) in (let H13 \def
 380 (eq_ind C c1 (\lambda (c: C).((eq C c (CHead e1 (Bind b1) v1)) \to (ex2_3 B C
 381 T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind
 382 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
 383 e2))))))) H2 e1 H10) in (let H14 \def (eq_ind C c1 (\lambda (c: C).(csuba g c
 384 c3)) H1 e1 H10) in (let H15 \def (eq_ind_r B b1 (\lambda (b: B).((eq C e1
 385 (CHead e1 (Bind b) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
 386 C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind b2) v2))))) (\lambda (_:
 387 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))) H13 Abst H9) in
 388 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
 389 (CHead c3 (Bind Abbr) u) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
 390 (e2: C).(\lambda (_: T).(csuba g e1 e2)))) Abbr c3 u (refl_equal C (CHead c3
 391 (Bind Abbr) u)) H14))))))))) H7)) H6)))))))))))) y c2 H0))) H)))))).
 392
 393 theorem csuba_gen_abst_rev:
 394  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
 395 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind
 396 Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))))))
 397 \def
 398  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
 399 (csuba g c (CHead d1 (Bind Abst) u))).(insert_eq C (CHead d1 (Bind Abst) u)
 400 (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(ex2 C (\lambda (d2: C).(eq
 401 C c (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (\lambda
 402 (y: C).(\lambda (H0: (csuba g c y)).(csuba_ind g (\lambda (c0: C).(\lambda
 403 (c1: C).((eq C c1 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda (d2: C).(eq C
 404 c0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))))) (\lambda
 405 (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abst) u))).(let H2
 406 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
 407 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
 408 False])) I (CHead d1 (Bind Abst) u) H1) in (False_ind (ex2 C (\lambda (d2:
 409 C).(eq C (CSort n) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
 410 d1))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
 411 c2)).(\lambda (H2: (((eq C c2 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda
 412 (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
 413 d1)))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c2 k u0)
 414 (CHead d1 (Bind Abst) u))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
 415 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
 416 _) \Rightarrow c0])) (CHead c2 k u0) (CHead d1 (Bind Abst) u) H3) in ((let H5
 417 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
 418 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
 419 u0) (CHead d1 (Bind Abst) u) H3) in ((let H6 \def (f_equal C T (\lambda (e:
 420 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
 421 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u0) (CHead d1 (Bind Abst) u) H3)
 422 in (\lambda (H7: (eq K k (Bind Abst))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r
 423 T u (\lambda (t: T).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k t) (CHead d2
 424 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (eq_ind_r K (Bind Abst)
 425 (\lambda (k0: K).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k0 u) (CHead d2
 426 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (let H9 \def (eq_ind C
 427 c2 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda
 428 (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
 429 d1))))) H2 d1 H8) in (let H10 \def (eq_ind C c2 (\lambda (c0: C).(csuba g c1
 430 c0)) H1 d1 H8) in (ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abst)
 431 u) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) c1
 432 (refl_equal C (CHead c1 (Bind Abst) u)) H10))) k H7) u0 H6)))) H5))
 433 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
 434 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda
 435 (d2: C).(eq C c1 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
 436 d1)))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
 437 a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
 438 (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Abst) u))).(let H6 \def (eq_ind C
 439 (CHead c2 (Bind Abbr) u0) (\lambda (ee: C).(match ee in C return (\lambda (_:
 440 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
 441 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
 442 return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow
 443 False | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead
 444 d1 (Bind Abst) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c1
 445 (Bind Abst) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
 446 H6)))))))))))) c y H0))) H))))).
 447
 448 theorem csuba_gen_void_rev:
 449  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c
 450 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind
 451 Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))))
 452 \def
 453  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
 454 (csuba g c (CHead d1 (Bind Void) u))).(insert_eq C (CHead d1 (Bind Void) u)
 455 (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(ex2 C (\lambda (d2: C).(eq
 456 C c (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) (\lambda
 457 (y: C).(\lambda (H0: (csuba g c y)).(csuba_ind g (\lambda (c0: C).(\lambda
 458 (c1: C).((eq C c1 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda (d2: C).(eq C
 459 c0 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))))) (\lambda
 460 (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Void) u))).(let H2
 461 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return (\lambda (_:
 462 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
 463 False])) I (CHead d1 (Bind Void) u) H1) in (False_ind (ex2 C (\lambda (d2:
 464 C).(eq C (CSort n) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
 465 d1))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1
 466 c2)).(\lambda (H2: (((eq C c2 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
 467 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
 468 d1)))))).(\lambda (k: K).(\lambda (u0: T).(\lambda (H3: (eq C (CHead c2 k u0)
 469 (CHead d1 (Bind Void) u))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
 470 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
 471 _) \Rightarrow c0])) (CHead c2 k u0) (CHead d1 (Bind Void) u) H3) in ((let H5
 472 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
 473 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
 474 u0) (CHead d1 (Bind Void) u) H3) in ((let H6 \def (f_equal C T (\lambda (e:
 475 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 |
 476 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u0) (CHead d1 (Bind Void) u) H3)
 477 in (\lambda (H7: (eq K k (Bind Void))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r
 478 T u (\lambda (t: T).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k t) (CHead d2
 479 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) (eq_ind_r K (Bind Void)
 480 (\lambda (k0: K).(ex2 C (\lambda (d2: C).(eq C (CHead c1 k0 u) (CHead d2
 481 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))) (let H9 \def (eq_ind C
 482 c2 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
 483 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
 484 d1))))) H2 d1 H8) in (let H10 \def (eq_ind C c2 (\lambda (c0: C).(csuba g c1
 485 c0)) H1 d1 H8) in (ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Void)
 486 u) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)) c1
 487 (refl_equal C (CHead c1 (Bind Void) u)) H10))) k H7) u0 H6)))) H5))
 488 H4))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (csuba g c1
 489 c2)).(\lambda (_: (((eq C c2 (CHead d1 (Bind Void) u)) \to (ex2 C (\lambda
 490 (d2: C).(eq C c1 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2
 491 d1)))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
 492 a))).(\lambda (u0: T).(\lambda (_: (arity g c2 u0 a)).(\lambda (H5: (eq C
 493 (CHead c2 (Bind Abbr) u0) (CHead d1 (Bind Void) u))).(let H6 \def (eq_ind C
 494 (CHead c2 (Bind Abbr) u0) (\lambda (ee: C).(match ee in C return (\lambda (_:
 495 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
 496 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
 497 return (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow
 498 False | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead
 499 d1 (Bind Void) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c1
 500 (Bind Abst) t) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1)))
 501 H6)))))))))))) c y H0))) H))))).
 502
 503 theorem csuba_gen_abbr_rev:
 504  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g c
 505 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2
 506 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
 507 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abst)
 508 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
 509 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
 510 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
 511 a))))))))))
 512 \def
 513  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
 514 (H: (csuba g c (CHead d1 (Bind Abbr) u1))).(insert_eq C (CHead d1 (Bind Abbr)
 515 u1) (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(or (ex2 C (\lambda (d2:
 516 C).(eq C c (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
 517 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead
 518 d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 519 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
 520 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
 521 (a: A).(arity g d1 u1 a))))))) (\lambda (y: C).(\lambda (H0: (csuba g c
 522 y)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c1 (CHead d1 (Bind
 523 Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind Abbr)
 524 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
 525 C).(\lambda (u2: T).(\lambda (_: A).(eq C c0 (CHead d2 (Bind Abst) u2)))))
 526 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
 527 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
 528 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))))))
 529 (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Bind Abbr)
 530 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
 531 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
 532 \Rightarrow False])) I (CHead d1 (Bind Abbr) u1) H1) in (False_ind (or (ex2 C
 533 (\lambda (d2: C).(eq C (CSort n) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
 534 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
 535 (_: A).(eq C (CSort n) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
 536 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
 537 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
 538 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) H2)))) (\lambda
 539 (c1: C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C
 540 c2 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead
 541 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
 542 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abst)
 543 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
 544 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
 545 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
 546 a))))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c2 k u)
 547 (CHead d1 (Bind Abbr) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match
 548 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
 549 _) \Rightarrow c0])) (CHead c2 k u) (CHead d1 (Bind Abbr) u1) H3) in ((let H5
 550 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
 551 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
 552 u) (CHead d1 (Bind Abbr) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
 553 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
 554 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u) (CHead d1 (Bind Abbr) u1) H3)
 555 in (\lambda (H7: (eq K k (Bind Abbr))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r
 556 T u1 (\lambda (t: T).(or (ex2 C (\lambda (d2: C).(eq C (CHead c1 k t) (CHead
 557 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
 558 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C (CHead c1 k t) (CHead d2 (Bind
 559 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
 560 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
 561 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
 562 u1 a))))))) (eq_ind_r K (Bind Abbr) (\lambda (k0: K).(or (ex2 C (\lambda (d2:
 563 C).(eq C (CHead c1 k0 u1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
 564 g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
 565 C (CHead c1 k0 u1) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda
 566 (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
 567 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
 568 (_: T).(\lambda (a: A).(arity g d1 u1 a))))))) (let H9 \def (eq_ind C c2
 569 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda
 570 (d2: C).(eq C c1 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
 571 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1
 572 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 573 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
 574 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
 575 (a: A).(arity g d1 u1 a)))))))) H2 d1 H8) in (let H10 \def (eq_ind C c2
 576 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H8) in (or_introl (ex2 C (\lambda
 577 (d2: C).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abbr) u1))) (\lambda
 578 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
 579 T).(\lambda (_: A).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind Abst)
 580 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
 581 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
 582 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
 583 (ex_intro2 C (\lambda (d2: C).(eq C (CHead c1 (Bind Abbr) u1) (CHead d2 (Bind
 584 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)) c1 (refl_equal C (CHead c1
 585 (Bind Abbr) u1)) H10)))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
 586 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c2
 587 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(eq C c1 (CHead d2
 588 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
 589 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1 (CHead d2 (Bind Abst)
 590 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
 591 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
 592 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
 593 a))))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (H3: (arity g c1 t (asucc
 594 g a))).(\lambda (u: T).(\lambda (H4: (arity g c2 u a)).(\lambda (H5: (eq C
 595 (CHead c2 (Bind Abbr) u) (CHead d1 (Bind Abbr) u1))).(let H6 \def (f_equal C
 596 C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
 597 \Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) (CHead c2 (Bind Abbr) u)
 598 (CHead d1 (Bind Abbr) u1) H5) in ((let H7 \def (f_equal C T (\lambda (e:
 599 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
 600 (CHead _ _ t0) \Rightarrow t0])) (CHead c2 (Bind Abbr) u) (CHead d1 (Bind
 601 Abbr) u1) H5) in (\lambda (H8: (eq C c2 d1)).(let H9 \def (eq_ind T u
 602 (\lambda (t0: T).(arity g c2 t0 a)) H4 u1 H7) in (let H10 \def (eq_ind C c2
 603 (\lambda (c0: C).(arity g c0 u1 a)) H9 d1 H8) in (let H11 \def (eq_ind C c2
 604 (\lambda (c0: C).((eq C c0 (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda
 605 (d2: C).(eq C c1 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
 606 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c1
 607 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 608 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
 609 A).(arity g d2 u2 (asucc g a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda
 610 (a0: A).(arity g d1 u1 a0)))))))) H2 d1 H8) in (let H12 \def (eq_ind C c2
 611 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H8) in (or_intror (ex2 C (\lambda
 612 (d2: C).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abbr) u1))) (\lambda
 613 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
 614 T).(\lambda (_: A).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst)
 615 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
 616 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 (asucc g
 617 a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1
 618 a0))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
 619 A).(eq C (CHead c1 (Bind Abst) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
 620 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
 621 C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 (asucc g a0))))) (\lambda
 622 (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 a0)))) c1 t a
 623 (refl_equal C (CHead c1 (Bind Abst) t)) H12 H3 H10)))))))) H6)))))))))))) c y
 624 H0))) H))))).
 625
 626 theorem csuba_gen_flat_rev:
 627  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
 628 (f: F).((csuba g c (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2:
 629 C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2:
 630 C).(\lambda (_: T).(csuba g d2 d1)))))))))
 631 \def
 632  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
 633 (f: F).(\lambda (H: (csuba g c (CHead d1 (Flat f) u1))).(insert_eq C (CHead
 634 d1 (Flat f) u1) (\lambda (c0: C).(csuba g c c0)) (\lambda (_: C).(ex2_2 C T
 635 (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda
 636 (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (y: C).(\lambda (H0:
 637 (csuba g c y)).(csuba_ind g (\lambda (c0: C).(\lambda (c1: C).((eq C c1
 638 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
 639 C c0 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
 640 d1))))))) (\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead d1 (Flat f)
 641 u1))).(let H2 \def (eq_ind C (CSort n) (\lambda (ee: C).(match ee in C return
 642 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
 643 \Rightarrow False])) I (CHead d1 (Flat f) u1) H1) in (False_ind (ex2_2 C T
 644 (\lambda (d2: C).(\lambda (u2: T).(eq C (CSort n) (CHead d2 (Flat f) u2))))
 645 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) H2)))) (\lambda (c1:
 646 C).(\lambda (c2: C).(\lambda (H1: (csuba g c1 c2)).(\lambda (H2: (((eq C c2
 647 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
 648 C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
 649 d1))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c2 k u)
 650 (CHead d1 (Flat f) u1))).(let H4 \def (f_equal C C (\lambda (e: C).(match e
 651 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _
 652 _) \Rightarrow c0])) (CHead c2 k u) (CHead d1 (Flat f) u1) H3) in ((let H5
 653 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K)
 654 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 k
 655 u) (CHead d1 (Flat f) u1) H3) in ((let H6 \def (f_equal C T (\lambda (e:
 656 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u |
 657 (CHead _ _ t) \Rightarrow t])) (CHead c2 k u) (CHead d1 (Flat f) u1) H3) in
 658 (\lambda (H7: (eq K k (Flat f))).(\lambda (H8: (eq C c2 d1)).(eq_ind_r T u1
 659 (\lambda (t: T).(ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1
 660 k t) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
 661 d1))))) (eq_ind_r K (Flat f) (\lambda (k0: K).(ex2_2 C T (\lambda (d2:
 662 C).(\lambda (u2: T).(eq C (CHead c1 k0 u1) (CHead d2 (Flat f) u2)))) (\lambda
 663 (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (let H9 \def (eq_ind C c2
 664 (\lambda (c0: C).((eq C c0 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda
 665 (d2: C).(\lambda (u2: T).(eq C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2:
 666 C).(\lambda (_: T).(csuba g d2 d1)))))) H2 d1 H8) in (let H10 \def (eq_ind C
 667 c2 (\lambda (c0: C).(csuba g c1 c0)) H1 d1 H8) in (ex2_2_intro C T (\lambda
 668 (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Flat f) u1) (CHead d2 (Flat f)
 669 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) c1 u1 (refl_equal C
 670 (CHead c1 (Flat f) u1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
 671 C).(\lambda (c2: C).(\lambda (_: (csuba g c1 c2)).(\lambda (_: (((eq C c2
 672 (CHead d1 (Flat f) u1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq
 673 C c1 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
 674 d1))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g
 675 a))).(\lambda (u: T).(\lambda (_: (arity g c2 u a)).(\lambda (H5: (eq C
 676 (CHead c2 (Bind Abbr) u) (CHead d1 (Flat f) u1))).(let H6 \def (eq_ind C
 677 (CHead c2 (Bind Abbr) u) (\lambda (ee: C).(match ee in C return (\lambda (_:
 678 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
 679 k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat
 680 _) \Rightarrow False])])) I (CHead d1 (Flat f) u1) H5) in (False_ind (ex2_2 C
 681 T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind Abst) t) (CHead d2
 682 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))
 683 H6)))))))))))) c y H0))) H)))))).
 684
 685 theorem csuba_gen_bind_rev:
 686  \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
 687 (v1: T).((csuba g c2 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2:
 688 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
 689 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))))))
 690 \def
 691  \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
 692 (v1: T).(\lambda (H: (csuba g c2 (CHead e1 (Bind b1) v1))).(insert_eq C
 693 (CHead e1 (Bind b1) v1) (\lambda (c: C).(csuba g c2 c)) (\lambda (_:
 694 C).(ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
 695 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 696 T).(csuba g e2 e1)))))) (\lambda (y: C).(\lambda (H0: (csuba g c2
 697 y)).(csuba_ind g (\lambda (c: C).(\lambda (c0: C).((eq C c0 (CHead e1 (Bind
 698 b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
 699 T).(eq C c (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
 700 C).(\lambda (_: T).(csuba g e2 e1)))))))) (\lambda (n: nat).(\lambda (H1: (eq
 701 C (CSort n) (CHead e1 (Bind b1) v1))).(let H2 \def (eq_ind C (CSort n)
 702 (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
 703 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind b1)
 704 v1) H1) in (False_ind (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
 705 (v2: T).(eq C (CSort n) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
 706 (e2: C).(\lambda (_: T).(csuba g e2 e1))))) H2)))) (\lambda (c1: C).(\lambda
 707 (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c3 (CHead e1
 708 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
 709 (v2: T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
 710 C).(\lambda (_: T).(csuba g e2 e1)))))))).(\lambda (k: K).(\lambda (u:
 711 T).(\lambda (H3: (eq C (CHead c3 k u) (CHead e1 (Bind b1) v1))).(let H4 \def
 712 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
 713 [(CSort _) \Rightarrow c3 | (CHead c _ _) \Rightarrow c])) (CHead c3 k u)
 714 (CHead e1 (Bind b1) v1) H3) in ((let H5 \def (f_equal C K (\lambda (e:
 715 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
 716 (CHead _ k0 _) \Rightarrow k0])) (CHead c3 k u) (CHead e1 (Bind b1) v1) H3)
 717 in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
 718 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
 719 (CHead c3 k u) (CHead e1 (Bind b1) v1) H3) in (\lambda (H7: (eq K k (Bind
 720 b1))).(\lambda (H8: (eq C c3 e1)).(eq_ind_r T v1 (\lambda (t: T).(ex2_3 B C T
 721 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 k t)
 722 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 723 T).(csuba g e2 e1)))))) (eq_ind_r K (Bind b1) (\lambda (k0: K).(ex2_3 B C T
 724 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 k0 v1)
 725 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 726 T).(csuba g e2 e1)))))) (let H9 \def (eq_ind C c3 (\lambda (c: C).((eq C c
 727 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
 728 C).(\lambda (v2: T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_:
 729 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))) H2 e1 H8) in (let
 730 H10 \def (eq_ind C c3 (\lambda (c: C).(csuba g c1 c)) H1 e1 H8) in
 731 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
 732 (CHead c1 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
 733 (e2: C).(\lambda (_: T).(csuba g e2 e1)))) b1 c1 v1 (refl_equal C (CHead c1
 734 (Bind b1) v1)) H10))) k H7) u H6)))) H5)) H4))))))))) (\lambda (c1:
 735 C).(\lambda (c3: C).(\lambda (H1: (csuba g c1 c3)).(\lambda (H2: (((eq C c3
 736 (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
 737 C).(\lambda (v2: T).(eq C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_:
 738 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1)))))))).(\lambda (t:
 739 T).(\lambda (a: A).(\lambda (_: (arity g c1 t (asucc g a))).(\lambda (u:
 740 T).(\lambda (H4: (arity g c3 u a)).(\lambda (H5: (eq C (CHead c3 (Bind Abbr)
 741 u) (CHead e1 (Bind b1) v1))).(let H6 \def (f_equal C C (\lambda (e: C).(match
 742 e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c3 | (CHead c _
 743 _) \Rightarrow c])) (CHead c3 (Bind Abbr) u) (CHead e1 (Bind b1) v1) H5) in
 744 ((let H7 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
 745 C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k
 746 in K return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _)
 747 \Rightarrow Abbr])])) (CHead c3 (Bind Abbr) u) (CHead e1 (Bind b1) v1) H5) in
 748 ((let H8 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
 749 C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead
 750 c3 (Bind Abbr) u) (CHead e1 (Bind b1) v1) H5) in (\lambda (H9: (eq B Abbr
 751 b1)).(\lambda (H10: (eq C c3 e1)).(let H11 \def (eq_ind T u (\lambda (t0:
 752 T).(arity g c3 t0 a)) H4 v1 H8) in (let H12 \def (eq_ind C c3 (\lambda (c:
 753 C).(arity g c v1 a)) H11 e1 H10) in (let H13 \def (eq_ind C c3 (\lambda (c:
 754 C).((eq C c (CHead e1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (b2:
 755 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c1 (CHead e2 (Bind b2) v2)))))
 756 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1))))))) H2 e1
 757 H10) in (let H14 \def (eq_ind C c3 (\lambda (c: C).(csuba g c1 c)) H1 e1 H10)
 758 in (let H15 \def (eq_ind_r B b1 (\lambda (b: B).((eq C e1 (CHead e1 (Bind b)
 759 v1)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq
 760 C c1 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda
 761 (_: T).(csuba g e2 e1))))))) H13 Abbr H9) in (ex2_3_intro B C T (\lambda (b2:
 762 B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c1 (Bind Abst) t) (CHead e2
 763 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g
 764 e2 e1)))) Abst c1 t (refl_equal C (CHead c1 (Bind Abst) t)) H14))))))))) H7))
 765 H6)))))))))))) c2 y H0))) H)))))).
 766