matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/fwd".
  18
  19 include "csuba/defs.ma".
  20
  21 theorem csuba_gen_abbr:
  22  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g
  23 (CHead d1 (Bind Abbr) u) c) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
  24 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))))
  25 \def
  26  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
  27 (csuba g (CHead d1 (Bind Abbr) u) c)).(let H0 \def (match H in csuba return
  28 (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0 c1)).((eq C c0
  29 (CHead d1 (Bind Abbr) u)) \to ((eq C c1 c) \to (ex2 C (\lambda (d2: C).(eq C
  30 c (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))))) with
  31 [(csuba_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead d1 (Bind
  32 Abbr) u))).(\lambda (H1: (eq C (CSort n) c)).((let H2 \def (eq_ind C (CSort
  33 n) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
  34 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead d1 (Bind Abbr)
  35 u) H0) in (False_ind ((eq C (CSort n) c) \to (ex2 C (\lambda (d2: C).(eq C c
  36 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) H2)) H1))) |
  37 (csuba_head c1 c2 H0 k u0) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u0)
  38 (CHead d1 (Bind Abbr) u))).(\lambda (H2: (eq C (CHead c2 k u0) c)).((let H3
  39 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
  40 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c1 k
  41 u0) (CHead d1 (Bind Abbr) u) H1) in ((let H4 \def (f_equal C K (\lambda (e:
  42 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
  43 (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u0) (CHead d1 (Bind Abbr) u) H1)
  44 in ((let H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
  45 (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0]))
  46 (CHead c1 k u0) (CHead d1 (Bind Abbr) u) H1) in (eq_ind C d1 (\lambda (c0:
  47 C).((eq K k (Bind Abbr)) \to ((eq T u0 u) \to ((eq C (CHead c2 k u0) c) \to
  48 ((csuba g c0 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Abbr)
  49 u))) (\lambda (d2: C).(csuba g d1 d2)))))))) (\lambda (H6: (eq K k (Bind
  50 Abbr))).(eq_ind K (Bind Abbr) (\lambda (k0: K).((eq T u0 u) \to ((eq C (CHead
  51 c2 k0 u0) c) \to ((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead
  52 d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))))) (\lambda (H7: (eq
  53 T u0 u)).(eq_ind T u (\lambda (t: T).((eq C (CHead c2 (Bind Abbr) t) c) \to
  54 ((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Abbr)
  55 u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda (H8: (eq C (CHead c2
  56 (Bind Abbr) u) c)).(eq_ind C (CHead c2 (Bind Abbr) u) (\lambda (c0:
  57 C).((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind
  58 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))) (\lambda (H9: (csuba g d1
  59 c2)).(ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u) (CHead d2
  60 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) c2 (refl_equal C (CHead c2
  61 (Bind Abbr) u)) H9)) c H8)) u0 (sym_eq T u0 u H7))) k (sym_eq K k (Bind Abbr)
  62 H6))) c1 (sym_eq C c1 d1 H5))) H4)) H3)) H2 H0))) | (csuba_abst c1 c2 H0 t a
  63 H1 u0 H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst) t) (CHead d1
  64 (Bind Abbr) u))).(\lambda (H4: (eq C (CHead c2 (Bind Abbr) u0) c)).((let H5
  65 \def (eq_ind C (CHead c1 (Bind Abst) t) (\lambda (e: C).(match e in C return
  66 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
  67 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
  68 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
  69 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
  70 \Rightarrow False])])) I (CHead d1 (Bind Abbr) u) H3) in (False_ind ((eq C
  71 (CHead c2 (Bind Abbr) u0) c) \to ((csuba g c1 c2) \to ((arity g c1 t (asucc g
  72 a)) \to ((arity g c2 u0 a) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
  73 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))))) H5)) H4 H0 H1 H2)))])
  74 in (H0 (refl_equal C (CHead d1 (Bind Abbr) u)) (refl_equal C c))))))).
  75
  76 theorem csuba_gen_void:
  77  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g
  78 (CHead d1 (Bind Void) u) c) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
  79 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))))))
  80 \def
  81  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u: T).(\lambda (H:
  82 (csuba g (CHead d1 (Bind Void) u) c)).(let H0 \def (match H in csuba return
  83 (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0 c1)).((eq C c0
  84 (CHead d1 (Bind Void) u)) \to ((eq C c1 c) \to (ex2 C (\lambda (d2: C).(eq C
  85 c (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))))))) with
  86 [(csuba_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead d1 (Bind
  87 Void) u))).(\lambda (H1: (eq C (CSort n) c)).((let H2 \def (eq_ind C (CSort
  88 n) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
  89 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead d1 (Bind Void)
  90 u) H0) in (False_ind ((eq C (CSort n) c) \to (ex2 C (\lambda (d2: C).(eq C c
  91 (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)))) H2)) H1))) |
  92 (csuba_head c1 c2 H0 k u0) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u0)
  93 (CHead d1 (Bind Void) u))).(\lambda (H2: (eq C (CHead c2 k u0) c)).((let H3
  94 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
  95 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c1 k
  96 u0) (CHead d1 (Bind Void) u) H1) in ((let H4 \def (f_equal C K (\lambda (e:
  97 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
  98 (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u0) (CHead d1 (Bind Void) u) H1)
  99 in ((let H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
 100 (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0]))
 101 (CHead c1 k u0) (CHead d1 (Bind Void) u) H1) in (eq_ind C d1 (\lambda (c0:
 102 C).((eq K k (Bind Void)) \to ((eq T u0 u) \to ((eq C (CHead c2 k u0) c) \to
 103 ((csuba g c0 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Void)
 104 u))) (\lambda (d2: C).(csuba g d1 d2)))))))) (\lambda (H6: (eq K k (Bind
 105 Void))).(eq_ind K (Bind Void) (\lambda (k0: K).((eq T u0 u) \to ((eq C (CHead
 106 c2 k0 u0) c) \to ((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead
 107 d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2))))))) (\lambda (H7: (eq
 108 T u0 u)).(eq_ind T u (\lambda (t: T).((eq C (CHead c2 (Bind Void) t) c) \to
 109 ((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Void)
 110 u))) (\lambda (d2: C).(csuba g d1 d2)))))) (\lambda (H8: (eq C (CHead c2
 111 (Bind Void) u) c)).(eq_ind C (CHead c2 (Bind Void) u) (\lambda (c0:
 112 C).((csuba g d1 c2) \to (ex2 C (\lambda (d2: C).(eq C c0 (CHead d2 (Bind
 113 Void) u))) (\lambda (d2: C).(csuba g d1 d2))))) (\lambda (H9: (csuba g d1
 114 c2)).(ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Void) u) (CHead d2
 115 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2)) c2 (refl_equal C (CHead c2
 116 (Bind Void) u)) H9)) c H8)) u0 (sym_eq T u0 u H7))) k (sym_eq K k (Bind Void)
 117 H6))) c1 (sym_eq C c1 d1 H5))) H4)) H3)) H2 H0))) | (csuba_abst c1 c2 H0 t a
 118 H1 u0 H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst) t) (CHead d1
 119 (Bind Void) u))).(\lambda (H4: (eq C (CHead c2 (Bind Abbr) u0) c)).((let H5
 120 \def (eq_ind C (CHead c1 (Bind Abst) t) (\lambda (e: C).(match e in C return
 121 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
 122 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b)
 123 \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow
 124 False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _)
 125 \Rightarrow False])])) I (CHead d1 (Bind Void) u) H3) in (False_ind ((eq C
 126 (CHead c2 (Bind Abbr) u0) c) \to ((csuba g c1 c2) \to ((arity g c1 t (asucc g
 127 a)) \to ((arity g c2 u0 a) \to (ex2 C (\lambda (d2: C).(eq C c (CHead d2
 128 (Bind Void) u))) (\lambda (d2: C).(csuba g d1 d2))))))) H5)) H4 H0 H1 H2)))])
 129 in (H0 (refl_equal C (CHead d1 (Bind Void) u)) (refl_equal C c))))))).
 130
 131 theorem csuba_gen_abst:
 132  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g
 133 (CHead d1 (Bind Abst) u1) c) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead
 134 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
 135 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr)
 136 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
 137 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
 138 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
 139 a))))))))))
 140 \def
 141  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
 142 (H: (csuba g (CHead d1 (Bind Abst) u1) c)).(let H0 \def (match H in csuba
 143 return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0 c1)).((eq C
 144 c0 (CHead d1 (Bind Abst) u1)) \to ((eq C c1 c) \to (or (ex2 C (\lambda (d2:
 145 C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
 146 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead
 147 d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 148 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
 149 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
 150 A).(arity g d2 u2 a))))))))))) with [(csuba_sort n) \Rightarrow (\lambda (H0:
 151 (eq C (CSort n) (CHead d1 (Bind Abst) u1))).(\lambda (H1: (eq C (CSort n)
 152 c)).((let H2 \def (eq_ind C (CSort n) (\lambda (e: C).(match e in C return
 153 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _)
 154 \Rightarrow False])) I (CHead d1 (Bind Abst) u1) H0) in (False_ind ((eq C
 155 (CSort n) c) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Abst)
 156 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
 157 C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr) u2)))))
 158 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
 159 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
 160 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))
 161 H2)) H1))) | (csuba_head c1 c2 H0 k u) \Rightarrow (\lambda (H1: (eq C (CHead
 162 c1 k u) (CHead d1 (Bind Abst) u1))).(\lambda (H2: (eq C (CHead c2 k u)
 163 c)).((let H3 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
 164 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t]))
 165 (CHead c1 k u) (CHead d1 (Bind Abst) u1) H1) in ((let H4 \def (f_equal C K
 166 (\lambda (e: C).(match e in C return (\lambda (_: C).K) with [(CSort _)
 167 \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u) (CHead d1
 168 (Bind Abst) u1) H1) in ((let H5 \def (f_equal C C (\lambda (e: C).(match e in
 169 C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _)
 170 \Rightarrow c0])) (CHead c1 k u) (CHead d1 (Bind Abst) u1) H1) in (eq_ind C
 171 d1 (\lambda (c0: C).((eq K k (Bind Abst)) \to ((eq T u u1) \to ((eq C (CHead
 172 c2 k u) c) \to ((csuba g c0 c2) \to (or (ex2 C (\lambda (d2: C).(eq C c
 173 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
 174 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind
 175 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
 176 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
 177 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
 178 a))))))))))) (\lambda (H6: (eq K k (Bind Abst))).(eq_ind K (Bind Abst)
 179 (\lambda (k0: K).((eq T u u1) \to ((eq C (CHead c2 k0 u) c) \to ((csuba g d1
 180 c2) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2 (Bind Abst) u1)))
 181 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
 182 (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
 183 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
 184 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
 185 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))))) (\lambda
 186 (H7: (eq T u u1)).(eq_ind T u1 (\lambda (t: T).((eq C (CHead c2 (Bind Abst)
 187 t) c) \to ((csuba g d1 c2) \to (or (ex2 C (\lambda (d2: C).(eq C c (CHead d2
 188 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
 189 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c (CHead d2 (Bind Abbr)
 190 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
 191 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
 192 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
 193 a))))))))) (\lambda (H8: (eq C (CHead c2 (Bind Abst) u1) c)).(eq_ind C (CHead
 194 c2 (Bind Abst) u1) (\lambda (c0: C).((csuba g d1 c2) \to (or (ex2 C (\lambda
 195 (d2: C).(eq C c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
 196 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c0
 197 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 198 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
 199 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
 200 A).(arity g d2 u2 a)))))))) (\lambda (H9: (csuba g d1 c2)).(or_introl (ex2 C
 201 (\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1) (CHead d2 (Bind Abst) u1)))
 202 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
 203 (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abst) u1) (CHead d2 (Bind Abbr)
 204 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
 205 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
 206 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
 207 a))))) (ex_intro2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abst) u1) (CHead
 208 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) c2 (refl_equal C
 209 (CHead c2 (Bind Abst) u1)) H9))) c H8)) u (sym_eq T u u1 H7))) k (sym_eq K k
 210 (Bind Abst) H6))) c1 (sym_eq C c1 d1 H5))) H4)) H3)) H2 H0))) | (csuba_abst
 211 c1 c2 H0 t a H1 u H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst)
 212 t) (CHead d1 (Bind Abst) u1))).(\lambda (H4: (eq C (CHead c2 (Bind Abbr) u)
 213 c)).((let H5 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
 214 (_: C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0]))
 215 (CHead c1 (Bind Abst) t) (CHead d1 (Bind Abst) u1) H3) in ((let H6 \def
 216 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
 217 [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 (Bind
 218 Abst) t) (CHead d1 (Bind Abst) u1) H3) in (eq_ind C d1 (\lambda (c0: C).((eq
 219 T t u1) \to ((eq C (CHead c2 (Bind Abbr) u) c) \to ((csuba g c0 c2) \to
 220 ((arity g c0 t (asucc g a)) \to ((arity g c2 u a) \to (or (ex2 C (\lambda
 221 (d2: C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
 222 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c
 223 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 224 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
 225 g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
 226 A).(arity g d2 u2 a0)))))))))))) (\lambda (H7: (eq T t u1)).(eq_ind T u1
 227 (\lambda (t0: T).((eq C (CHead c2 (Bind Abbr) u) c) \to ((csuba g d1 c2) \to
 228 ((arity g d1 t0 (asucc g a)) \to ((arity g c2 u a) \to (or (ex2 C (\lambda
 229 (d2: C).(eq C c (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
 230 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c
 231 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 232 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
 233 g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
 234 A).(arity g d2 u2 a0))))))))))) (\lambda (H8: (eq C (CHead c2 (Bind Abbr) u)
 235 c)).(eq_ind C (CHead c2 (Bind Abbr) u) (\lambda (c0: C).((csuba g d1 c2) \to
 236 ((arity g d1 u1 (asucc g a)) \to ((arity g c2 u a) \to (or (ex2 C (\lambda
 237 (d2: C).(eq C c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
 238 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c0
 239 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
 240 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity
 241 g d1 u1 (asucc g a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0:
 242 A).(arity g d2 u2 a0)))))))))) (\lambda (H9: (csuba g d1 c2)).(\lambda (H10:
 243 (arity g d1 u1 (asucc g a))).(\lambda (H11: (arity g c2 u a)).(or_intror (ex2
 244 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abst) u1)))
 245 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
 246 (u2: T).(\lambda (_: A).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abbr)
 247 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
 248 (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g
 249 a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2
 250 a0))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
 251 A).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
 252 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
 253 C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 u1 (asucc g a0))))) (\lambda
 254 (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 a0)))) c2 u a
 255 (refl_equal C (CHead c2 (Bind Abbr) u)) H9 H10 H11))))) c H8)) t (sym_eq T t
 256 u1 H7))) c1 (sym_eq C c1 d1 H6))) H5)) H4 H0 H1 H2)))]) in (H0 (refl_equal C
 257 (CHead d1 (Bind Abst) u1)) (refl_equal C c))))))).
 258
 259 theorem csuba_gen_flat:
 260  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall
 261 (f: F).((csuba g (CHead d1 (Flat f) u1) c) \to (ex2_2 C T (\lambda (d2:
 262 C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2:
 263 C).(\lambda (_: T).(csuba g d1 d2)))))))))
 264 \def
 265  \lambda (g: G).(\lambda (d1: C).(\lambda (c: C).(\lambda (u1: T).(\lambda
 266 (f: F).(\lambda (H: (csuba g (CHead d1 (Flat f) u1) c)).(let H0 \def (match H
 267 in csuba return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csuba ? c0
 268 c1)).((eq C c0 (CHead d1 (Flat f) u1)) \to ((eq C c1 c) \to (ex2_2 C T
 269 (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda
 270 (d2: C).(\lambda (_: T).(csuba g d1 d2))))))))) with [(csuba_sort n)
 271 \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead d1 (Flat f) u1))).(\lambda
 272 (H1: (eq C (CSort n) c)).((let H2 \def (eq_ind C (CSort n) (\lambda (e:
 273 C).(match e in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
 274 True | (CHead _ _ _) \Rightarrow False])) I (CHead d1 (Flat f) u1) H0) in
 275 (False_ind ((eq C (CSort n) c) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
 276 T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
 277 g d1 d2))))) H2)) H1))) | (csuba_head c1 c2 H0 k u) \Rightarrow (\lambda (H1:
 278 (eq C (CHead c1 k u) (CHead d1 (Flat f) u1))).(\lambda (H2: (eq C (CHead c2 k
 279 u) c)).((let H3 \def (f_equal C T (\lambda (e: C).(match e in C return
 280 (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow
 281 t])) (CHead c1 k u) (CHead d1 (Flat f) u1) H1) in ((let H4 \def (f_equal C K
 282 (\lambda (e: C).(match e in C return (\lambda (_: C).K) with [(CSort _)
 283 \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u) (CHead d1
 284 (Flat f) u1) H1) in ((let H5 \def (f_equal C C (\lambda (e: C).(match e in C
 285 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _)
 286 \Rightarrow c0])) (CHead c1 k u) (CHead d1 (Flat f) u1) H1) in (eq_ind C d1
 287 (\lambda (c0: C).((eq K k (Flat f)) \to ((eq T u u1) \to ((eq C (CHead c2 k
 288 u) c) \to ((csuba g c0 c2) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
 289 T).(eq C c (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
 290 g d1 d2))))))))) (\lambda (H6: (eq K k (Flat f))).(eq_ind K (Flat f) (\lambda
 291 (k0: K).((eq T u u1) \to ((eq C (CHead c2 k0 u) c) \to ((csuba g d1 c2) \to
 292 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2 (Flat f)
 293 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))))))) (\lambda (H7:
 294 (eq T u u1)).(eq_ind T u1 (\lambda (t: T).((eq C (CHead c2 (Flat f) t) c) \to
 295 ((csuba g d1 c2) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c
 296 (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
 297 d2))))))) (\lambda (H8: (eq C (CHead c2 (Flat f) u1) c)).(eq_ind C (CHead c2
 298 (Flat f) u1) (\lambda (c0: C).((csuba g d1 c2) \to (ex2_2 C T (\lambda (d2:
 299 C).(\lambda (u2: T).(eq C c0 (CHead d2 (Flat f) u2)))) (\lambda (d2:
 300 C).(\lambda (_: T).(csuba g d1 d2)))))) (\lambda (H9: (csuba g d1
 301 c2)).(ex2_2_intro C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Flat
 302 f) u1) (CHead d2 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1
 303 d2))) c2 u1 (refl_equal C (CHead c2 (Flat f) u1)) H9)) c H8)) u (sym_eq T u
 304 u1 H7))) k (sym_eq K k (Flat f) H6))) c1 (sym_eq C c1 d1 H5))) H4)) H3)) H2
 305 H0))) | (csuba_abst c1 c2 H0 t a H1 u H2) \Rightarrow (\lambda (H3: (eq C
 306 (CHead c1 (Bind Abst) t) (CHead d1 (Flat f) u1))).(\lambda (H4: (eq C (CHead
 307 c2 (Bind Abbr) u) c)).((let H5 \def (eq_ind C (CHead c1 (Bind Abst) t)
 308 (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
 309 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
 310 (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
 311 False])])) I (CHead d1 (Flat f) u1) H3) in (False_ind ((eq C (CHead c2 (Bind
 312 Abbr) u) c) \to ((csuba g c1 c2) \to ((arity g c1 t (asucc g a)) \to ((arity
 313 g c2 u a) \to (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C c (CHead d2
 314 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))))))) H5))
 315 H4 H0 H1 H2)))]) in (H0 (refl_equal C (CHead d1 (Flat f) u1)) (refl_equal C
 316 c)))))))).
 317
 318 theorem csuba_gen_bind:
 319  \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
 320 (v1: T).((csuba g (CHead e1 (Bind b1) v1) c2) \to (ex2_3 B C T (\lambda (b2:
 321 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
 322 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))))))
 323 \def
 324  \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
 325 (v1: T).(\lambda (H: (csuba g (CHead e1 (Bind b1) v1) c2)).(let H0 \def
 326 (match H in csuba return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csuba
 327 ? c c0)).((eq C c (CHead e1 (Bind b1) v1)) \to ((eq C c0 c2) \to (ex2_3 B C T
 328 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
 329 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
 330 e2)))))))))) with [(csuba_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n)
 331 (CHead e1 (Bind b1) v1))).(\lambda (H1: (eq C (CSort n) c2)).((let H2 \def
 332 (eq_ind C (CSort n) (\lambda (e: C).(match e in C return (\lambda (_:
 333 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
 334 False])) I (CHead e1 (Bind b1) v1) H0) in (False_ind ((eq C (CSort n) c2) \to
 335 (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
 336 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 337 T).(csuba g e1 e2)))))) H2)) H1))) | (csuba_head c1 c0 H0 k u) \Rightarrow
 338 (\lambda (H1: (eq C (CHead c1 k u) (CHead e1 (Bind b1) v1))).(\lambda (H2:
 339 (eq C (CHead c0 k u) c2)).((let H3 \def (f_equal C T (\lambda (e: C).(match e
 340 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t)
 341 \Rightarrow t])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H1) in ((let H4 \def
 342 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
 343 [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u)
 344 (CHead e1 (Bind b1) v1) H1) in ((let H5 \def (f_equal C C (\lambda (e:
 345 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 |
 346 (CHead c _ _) \Rightarrow c])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H1) in
 347 (eq_ind C e1 (\lambda (c: C).((eq K k (Bind b1)) \to ((eq T u v1) \to ((eq C
 348 (CHead c0 k u) c2) \to ((csuba g c c0) \to (ex2_3 B C T (\lambda (b2:
 349 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
 350 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2))))))))))
 351 (\lambda (H6: (eq K k (Bind b1))).(eq_ind K (Bind b1) (\lambda (k0: K).((eq T
 352 u v1) \to ((eq C (CHead c0 k0 u) c2) \to ((csuba g e1 c0) \to (ex2_3 B C T
 353 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
 354 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
 355 e2))))))))) (\lambda (H7: (eq T u v1)).(eq_ind T v1 (\lambda (t: T).((eq C
 356 (CHead c0 (Bind b1) t) c2) \to ((csuba g e1 c0) \to (ex2_3 B C T (\lambda
 357 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2)
 358 v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
 359 e2)))))))) (\lambda (H8: (eq C (CHead c0 (Bind b1) v1) c2)).(eq_ind C (CHead
 360 c0 (Bind b1) v1) (\lambda (c: C).((csuba g e1 c0) \to (ex2_3 B C T (\lambda
 361 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c (CHead e2 (Bind b2) v2)))))
 362 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2)))))))
 363 (\lambda (H9: (csuba g e1 c0)).(let H10 \def (eq_ind_r C c2 (\lambda (c:
 364 C).(csuba g (CHead e1 (Bind b1) v1) c)) H (CHead c0 (Bind b1) v1) H8) in
 365 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
 366 (CHead c0 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
 367 (e2: C).(\lambda (_: T).(csuba g e1 e2)))) b1 c0 v1 (refl_equal C (CHead c0
 368 (Bind b1) v1)) H9))) c2 H8)) u (sym_eq T u v1 H7))) k (sym_eq K k (Bind b1)
 369 H6))) c1 (sym_eq C c1 e1 H5))) H4)) H3)) H2 H0))) | (csuba_abst c1 c0 H0 t a
 370 H1 u H2) \Rightarrow (\lambda (H3: (eq C (CHead c1 (Bind Abst) t) (CHead e1
 371 (Bind b1) v1))).(\lambda (H4: (eq C (CHead c0 (Bind Abbr) u) c2)).((let H5
 372 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
 373 with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (CHead c1
 374 (Bind Abst) t) (CHead e1 (Bind b1) v1) H3) in ((let H6 \def (f_equal C B
 375 (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _)
 376 \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k in K return (\lambda
 377 (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abst])]))
 378 (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H3) in ((let H7 \def
 379 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
 380 [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 (Bind
 381 Abst) t) (CHead e1 (Bind b1) v1) H3) in (eq_ind C e1 (\lambda (c: C).((eq B
 382 Abst b1) \to ((eq T t v1) \to ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csuba
 383 g c c0) \to ((arity g c t (asucc g a)) \to ((arity g c0 u a) \to (ex2_3 B C T
 384 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
 385 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
 386 e2)))))))))))) (\lambda (H8: (eq B Abst b1)).(eq_ind B Abst (\lambda (_:
 387 B).((eq T t v1) \to ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csuba g e1 c0)
 388 \to ((arity g e1 t (asucc g a)) \to ((arity g c0 u a) \to (ex2_3 B C T
 389 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
 390 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1
 391 e2))))))))))) (\lambda (H9: (eq T t v1)).(eq_ind T v1 (\lambda (t0: T).((eq C
 392 (CHead c0 (Bind Abbr) u) c2) \to ((csuba g e1 c0) \to ((arity g e1 t0 (asucc
 393 g a)) \to ((arity g c0 u a) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
 394 C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2))))) (\lambda (_:
 395 B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2)))))))))) (\lambda (H10:
 396 (eq C (CHead c0 (Bind Abbr) u) c2)).(eq_ind C (CHead c0 (Bind Abbr) u)
 397 (\lambda (c: C).((csuba g e1 c0) \to ((arity g e1 v1 (asucc g a)) \to ((arity
 398 g c0 u a) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
 399 T).(eq C c (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
 400 C).(\lambda (_: T).(csuba g e1 e2))))))))) (\lambda (H11: (csuba g e1
 401 c0)).(\lambda (_: (arity g e1 v1 (asucc g a))).(\lambda (_: (arity g c0 u
 402 a)).(let H14 \def (eq_ind_r C c2 (\lambda (c: C).(csuba g (CHead e1 (Bind b1)
 403 v1) c)) H (CHead c0 (Bind Abbr) u) H10) in (let H15 \def (eq_ind_r B b1
 404 (\lambda (b: B).(csuba g (CHead e1 (Bind b) v1) (CHead c0 (Bind Abbr) u)))
 405 H14 Abst H8) in (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
 406 (v2: T).(eq C (CHead c0 (Bind Abbr) u) (CHead e2 (Bind b2) v2))))) (\lambda
 407 (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e1 e2)))) Abbr c0 u
 408 (refl_equal C (CHead c0 (Bind Abbr) u)) H11)))))) c2 H10)) t (sym_eq T t v1
 409 H9))) b1 H8)) c1 (sym_eq C c1 e1 H7))) H6)) H5)) H4 H0 H1 H2)))]) in (H0
 410 (refl_equal C (CHead e1 (Bind b1) v1)) (refl_equal C c2)))))))).
 411