matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/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/csub3/fwd".
  18
  19 include "csub3/defs.ma".
  20
  21 theorem csub3_gen_abbr:
  22  \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v: T).((csub3 g
  23 (CHead e1 (Bind Abbr) v) c2) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2
  24 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2)))))))
  25 \def
  26  \lambda (g: G).(\lambda (e1: C).(\lambda (c2: C).(\lambda (v: T).(\lambda
  27 (H: (csub3 g (CHead e1 (Bind Abbr) v) c2)).(let H0 \def (match H in csub3
  28 return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csub3 ? c c0)).((eq C c
  29 (CHead e1 (Bind Abbr) v)) \to ((eq C c0 c2) \to (ex2 C (\lambda (e2: C).(eq C
  30 c2 (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2)))))))) with
  31 [(csub3_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead e1 (Bind
  32 Abbr) v))).(\lambda (H1: (eq C (CSort n) c2)).((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 e1 (Bind Abbr)
  35 v) H0) in (False_ind ((eq C (CSort n) c2) \to (ex2 C (\lambda (e2: C).(eq C
  36 c2 (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2)))) H2)) H1)))
  37 | (csub3_head c1 c0 H0 k u) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u)
  38 (CHead e1 (Bind Abbr) v))).(\lambda (H2: (eq C (CHead c0 k u) c2)).((let H3
  39 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
  40 with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c1 k u)
  41 (CHead e1 (Bind Abbr) v) 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 u) (CHead e1 (Bind Abbr) v) 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 c _ _) \Rightarrow c]))
  46 (CHead c1 k u) (CHead e1 (Bind Abbr) v) H1) in (eq_ind C e1 (\lambda (c:
  47 C).((eq K k (Bind Abbr)) \to ((eq T u v) \to ((eq C (CHead c0 k u) c2) \to
  48 ((csub3 g c c0) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abbr)
  49 v))) (\lambda (e2: C).(csub3 g e1 e2)))))))) (\lambda (H6: (eq K k (Bind
  50 Abbr))).(eq_ind K (Bind Abbr) (\lambda (k0: K).((eq T u v) \to ((eq C (CHead
  51 c0 k0 u) c2) \to ((csub3 g e1 c0) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead
  52 e2 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2))))))) (\lambda (H7: (eq
  53 T u v)).(eq_ind T v (\lambda (t: T).((eq C (CHead c0 (Bind Abbr) t) c2) \to
  54 ((csub3 g e1 c0) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abbr)
  55 v))) (\lambda (e2: C).(csub3 g e1 e2)))))) (\lambda (H8: (eq C (CHead c0
  56 (Bind Abbr) v) c2)).(eq_ind C (CHead c0 (Bind Abbr) v) (\lambda (c:
  57 C).((csub3 g e1 c0) \to (ex2 C (\lambda (e2: C).(eq C c (CHead e2 (Bind Abbr)
  58 v))) (\lambda (e2: C).(csub3 g e1 e2))))) (\lambda (H9: (csub3 g e1 c0)).(let
  59 H10 \def (eq_ind_r C c2 (\lambda (c: C).(csub3 g (CHead e1 (Bind Abbr) v) c))
  60 H (CHead c0 (Bind Abbr) v) H8) in (ex_intro2 C (\lambda (e2: C).(eq C (CHead
  61 c0 (Bind Abbr) v) (CHead e2 (Bind Abbr) v))) (\lambda (e2: C).(csub3 g e1
  62 e2)) c0 (refl_equal C (CHead c0 (Bind Abbr) v)) H9))) c2 H8)) u (sym_eq T u v
  63 H7))) k (sym_eq K k (Bind Abbr) H6))) c1 (sym_eq C c1 e1 H5))) H4)) H3)) H2
  64 H0))) | (csub3_void c1 c0 H0 b H1 u1 u2) \Rightarrow (\lambda (H2: (eq C
  65 (CHead c1 (Bind Void) u1) (CHead e1 (Bind Abbr) v))).(\lambda (H3: (eq C
  66 (CHead c0 (Bind b) u2) c2)).((let H4 \def (eq_ind C (CHead c1 (Bind Void) u1)
  67 (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
  68 \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda
  69 (_: K).Prop) with [(Bind b0) \Rightarrow (match b0 in B return (\lambda (_:
  70 B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow False | Void
  71 \Rightarrow True]) | (Flat _) \Rightarrow False])])) I (CHead e1 (Bind Abbr)
  72 v) H2) in (False_ind ((eq C (CHead c0 (Bind b) u2) c2) \to ((csub3 g c1 c0)
  73 \to ((not (eq B b Void)) \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind
  74 Abbr) v))) (\lambda (e2: C).(csub3 g e1 e2)))))) H4)) H3 H0 H1))) |
  75 (csub3_abst c1 c0 H0 u t H1) \Rightarrow (\lambda (H2: (eq C (CHead c1 (Bind
  76 Abst) t) (CHead e1 (Bind Abbr) v))).(\lambda (H3: (eq C (CHead c0 (Bind Abbr)
  77 u) c2)).((let H4 \def (eq_ind C (CHead c1 (Bind Abst) t) (\lambda (e:
  78 C).(match e in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
  79 False | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop)
  80 with [(Bind b) \Rightarrow (match b in B return (\lambda (_: B).Prop) with
  81 [Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) |
  82 (Flat _) \Rightarrow False])])) I (CHead e1 (Bind Abbr) v) H2) in (False_ind
  83 ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g c1 c0) \to ((ty3 g c0 u t)
  84 \to (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abbr) v))) (\lambda (e2:
  85 C).(csub3 g e1 e2)))))) H4)) H3 H0 H1)))]) in (H0 (refl_equal C (CHead e1
  86 (Bind Abbr) v)) (refl_equal C c2))))))).
  87
  88 theorem csub3_gen_abst:
  89  \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v1: T).((csub3 g
  90 (CHead e1 (Bind Abst) v1) c2) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead
  91 e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda
  92 (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
  93 C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
  94 e2 v2 v1)))))))))
  95 \def
  96  \lambda (g: G).(\lambda (e1: C).(\lambda (c2: C).(\lambda (v1: T).(\lambda
  97 (H: (csub3 g (CHead e1 (Bind Abst) v1) c2)).(let H0 \def (match H in csub3
  98 return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csub3 ? c c0)).((eq C c
  99 (CHead e1 (Bind Abst) v1)) \to ((eq C c0 c2) \to (or (ex2 C (\lambda (e2:
 100 C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2)))
 101 (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr)
 102 v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2:
 103 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))))) with [(csub3_sort n)
 104 \Rightarrow (\lambda (H0: (eq C (CSort n) (CHead e1 (Bind Abst)
 105 v1))).(\lambda (H1: (eq C (CSort n) c2)).((let H2 \def (eq_ind C (CSort n)
 106 (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with [(CSort _)
 107 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind Abst)
 108 v1) H0) in (False_ind ((eq C (CSort n) c2) \to (or (ex2 C (\lambda (e2:
 109 C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2)))
 110 (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr)
 111 v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2:
 112 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))) H2)) H1))) | (csub3_head c1 c0 H0 k
 113 u) \Rightarrow (\lambda (H1: (eq C (CHead c1 k u) (CHead e1 (Bind Abst)
 114 v1))).(\lambda (H2: (eq C (CHead c0 k u) c2)).((let H3 \def (f_equal C T
 115 (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
 116 \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c1 k u) (CHead e1 (Bind
 117 Abst) v1) H1) in ((let H4 \def (f_equal C K (\lambda (e: C).(match e in C
 118 return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _)
 119 \Rightarrow k0])) (CHead c1 k u) (CHead e1 (Bind Abst) v1) H1) in ((let H5
 120 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
 121 with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead c1 k
 122 u) (CHead e1 (Bind Abst) v1) H1) in (eq_ind C e1 (\lambda (c: C).((eq K k
 123 (Bind Abst)) \to ((eq T u v1) \to ((eq C (CHead c0 k u) c2) \to ((csub3 g c
 124 c0) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1)))
 125 (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2:
 126 T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
 127 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
 128 v1)))))))))) (\lambda (H6: (eq K k (Bind Abst))).(eq_ind K (Bind Abst)
 129 (\lambda (k0: K).((eq T u v1) \to ((eq C (CHead c0 k0 u) c2) \to ((csub3 g e1
 130 c0) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1)))
 131 (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2:
 132 T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
 133 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
 134 v1))))))))) (\lambda (H7: (eq T u v1)).(eq_ind T v1 (\lambda (t: T).((eq C
 135 (CHead c0 (Bind Abst) t) c2) \to ((csub3 g e1 c0) \to (or (ex2 C (\lambda
 136 (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1
 137 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
 138 Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2:
 139 C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))) (\lambda (H8: (eq C (CHead c0
 140 (Bind Abst) v1) c2)).(eq_ind C (CHead c0 (Bind Abst) v1) (\lambda (c:
 141 C).((csub3 g e1 c0) \to (or (ex2 C (\lambda (e2: C).(eq C c (CHead e2 (Bind
 142 Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2:
 143 C).(\lambda (v2: T).(eq C c (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
 144 C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
 145 e2 v2 v1))))))) (\lambda (H9: (csub3 g e1 c0)).(let H10 \def (eq_ind_r C c2
 146 (\lambda (c: C).(csub3 g (CHead e1 (Bind Abst) v1) c)) H (CHead c0 (Bind
 147 Abst) v1) H8) in (or_introl (ex2 C (\lambda (e2: C).(eq C (CHead c0 (Bind
 148 Abst) v1) (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2)))
 149 (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c0 (Bind Abst) v1)
 150 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1
 151 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1)))) (ex_intro2 C
 152 (\lambda (e2: C).(eq C (CHead c0 (Bind Abst) v1) (CHead e2 (Bind Abst) v1)))
 153 (\lambda (e2: C).(csub3 g e1 e2)) c0 (refl_equal C (CHead c0 (Bind Abst) v1))
 154 H9)))) c2 H8)) u (sym_eq T u v1 H7))) k (sym_eq K k (Bind Abst) H6))) c1
 155 (sym_eq C c1 e1 H5))) H4)) H3)) H2 H0))) | (csub3_void c1 c0 H0 b H1 u1 u2)
 156 \Rightarrow (\lambda (H2: (eq C (CHead c1 (Bind Void) u1) (CHead e1 (Bind
 157 Abst) v1))).(\lambda (H3: (eq C (CHead c0 (Bind b) u2) c2)).((let H4 \def
 158 (eq_ind C (CHead c1 (Bind Void) u1) (\lambda (e: C).(match e in C return
 159 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _)
 160 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind b0)
 161 \Rightarrow (match b0 in B return (\lambda (_: B).Prop) with [Abbr
 162 \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow True]) | (Flat
 163 _) \Rightarrow False])])) I (CHead e1 (Bind Abst) v1) H2) in (False_ind ((eq
 164 C (CHead c0 (Bind b) u2) c2) \to ((csub3 g c1 c0) \to ((not (eq B b Void))
 165 \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda
 166 (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C
 167 c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csub3 g e1
 168 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))) H4)) H3 H0
 169 H1))) | (csub3_abst c1 c0 H0 u t H1) \Rightarrow (\lambda (H2: (eq C (CHead
 170 c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1))).(\lambda (H3: (eq C (CHead c0
 171 (Bind Abbr) u) c2)).((let H4 \def (f_equal C T (\lambda (e: C).(match e in C
 172 return (\lambda (_: C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t0)
 173 \Rightarrow t0])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1) H2) in
 174 ((let H5 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_:
 175 C).C) with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead
 176 c1 (Bind Abst) t) (CHead e1 (Bind Abst) v1) H2) in (eq_ind C e1 (\lambda (c:
 177 C).((eq T t v1) \to ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g c c0)
 178 \to ((ty3 g c0 u t) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind
 179 Abst) v1))) (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2:
 180 C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
 181 C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
 182 e2 v2 v1)))))))))) (\lambda (H6: (eq T t v1)).(eq_ind T v1 (\lambda (t0:
 183 T).((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g e1 c0) \to ((ty3 g c0 u
 184 t0) \to (or (ex2 C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) v1)))
 185 (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2:
 186 T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
 187 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
 188 v1))))))))) (\lambda (H7: (eq C (CHead c0 (Bind Abbr) u) c2)).(eq_ind C
 189 (CHead c0 (Bind Abbr) u) (\lambda (c: C).((csub3 g e1 c0) \to ((ty3 g c0 u
 190 v1) \to (or (ex2 C (\lambda (e2: C).(eq C c (CHead e2 (Bind Abst) v1)))
 191 (\lambda (e2: C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2:
 192 T).(eq C c (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
 193 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
 194 v1)))))))) (\lambda (H8: (csub3 g e1 c0)).(\lambda (H9: (ty3 g c0 u v1)).(let
 195 H10 \def (eq_ind_r C c2 (\lambda (c: C).(csub3 g (CHead e1 (Bind Abst) v1)
 196 c)) H (CHead c0 (Bind Abbr) u) H7) in (or_intror (ex2 C (\lambda (e2: C).(eq
 197 C (CHead c0 (Bind Abbr) u) (CHead e2 (Bind Abst) v1))) (\lambda (e2:
 198 C).(csub3 g e1 e2))) (ex3_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C
 199 (CHead c0 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
 200 C).(\lambda (_: T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g
 201 e2 v2 v1)))) (ex3_2_intro C T (\lambda (e2: C).(\lambda (v2: T).(eq C (CHead
 202 c0 (Bind Abbr) u) (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
 203 T).(csub3 g e1 e2))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1))) c0
 204 u (refl_equal C (CHead c0 (Bind Abbr) u)) H8 H9))))) c2 H7)) t (sym_eq T t v1
 205 H6))) c1 (sym_eq C c1 e1 H5))) H4)) H3 H0 H1)))]) in (H0 (refl_equal C (CHead
 206 e1 (Bind Abst) v1)) (refl_equal C c2))))))).
 207
 208 theorem csub3_gen_bind:
 209  \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall
 210 (v1: T).((csub3 g (CHead e1 (Bind b1) v1) c2) \to (ex2_3 B C T (\lambda (b2:
 211 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
 212 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))))))))))
 213 \def
 214  \lambda (g: G).(\lambda (b1: B).(\lambda (e1: C).(\lambda (c2: C).(\lambda
 215 (v1: T).(\lambda (H: (csub3 g (CHead e1 (Bind b1) v1) c2)).(let H0 \def
 216 (match H in csub3 return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csub3
 217 ? c c0)).((eq C c (CHead e1 (Bind b1) v1)) \to ((eq C c0 c2) \to (ex2_3 B C T
 218 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
 219 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1
 220 e2)))))))))) with [(csub3_sort n) \Rightarrow (\lambda (H0: (eq C (CSort n)
 221 (CHead e1 (Bind b1) v1))).(\lambda (H1: (eq C (CSort n) c2)).((let H2 \def
 222 (eq_ind C (CSort n) (\lambda (e: C).(match e in C return (\lambda (_:
 223 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
 224 False])) I (CHead e1 (Bind b1) v1) H0) in (False_ind ((eq C (CSort n) c2) \to
 225 (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
 226 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 227 T).(csub3 g e1 e2)))))) H2)) H1))) | (csub3_head c1 c0 H0 k u) \Rightarrow
 228 (\lambda (H1: (eq C (CHead c1 k u) (CHead e1 (Bind b1) v1))).(\lambda (H2:
 229 (eq C (CHead c0 k u) c2)).((let H3 \def (f_equal C T (\lambda (e: C).(match e
 230 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t)
 231 \Rightarrow t])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H1) in ((let H4 \def
 232 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
 233 [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c1 k u)
 234 (CHead e1 (Bind b1) v1) H1) in ((let H5 \def (f_equal C C (\lambda (e:
 235 C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1 |
 236 (CHead c _ _) \Rightarrow c])) (CHead c1 k u) (CHead e1 (Bind b1) v1) H1) in
 237 (eq_ind C e1 (\lambda (c: C).((eq K k (Bind b1)) \to ((eq T u v1) \to ((eq C
 238 (CHead c0 k u) c2) \to ((csub3 g c c0) \to (ex2_3 B C T (\lambda (b2:
 239 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
 240 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))))))))))
 241 (\lambda (H6: (eq K k (Bind b1))).(eq_ind K (Bind b1) (\lambda (k0: K).((eq T
 242 u v1) \to ((eq C (CHead c0 k0 u) c2) \to ((csub3 g e1 c0) \to (ex2_3 B C T
 243 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
 244 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1
 245 e2))))))))) (\lambda (H7: (eq T u v1)).(eq_ind T v1 (\lambda (t: T).((eq C
 246 (CHead c0 (Bind b1) t) c2) \to ((csub3 g e1 c0) \to (ex2_3 B C T (\lambda
 247 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2)
 248 v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1
 249 e2)))))))) (\lambda (H8: (eq C (CHead c0 (Bind b1) v1) c2)).(eq_ind C (CHead
 250 c0 (Bind b1) v1) (\lambda (c: C).((csub3 g e1 c0) \to (ex2_3 B C T (\lambda
 251 (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c (CHead e2 (Bind b2) v2)))))
 252 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2)))))))
 253 (\lambda (H9: (csub3 g e1 c0)).(let H10 \def (eq_ind_r C c2 (\lambda (c:
 254 C).(csub3 g (CHead e1 (Bind b1) v1) c)) H (CHead c0 (Bind b1) v1) H8) in
 255 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
 256 (CHead c0 (Bind b1) v1) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
 257 (e2: C).(\lambda (_: T).(csub3 g e1 e2)))) b1 c0 v1 (refl_equal C (CHead c0
 258 (Bind b1) v1)) H9))) c2 H8)) u (sym_eq T u v1 H7))) k (sym_eq K k (Bind b1)
 259 H6))) c1 (sym_eq C c1 e1 H5))) H4)) H3)) H2 H0))) | (csub3_void c1 c0 H0 b H1
 260 u1 u2) \Rightarrow (\lambda (H2: (eq C (CHead c1 (Bind Void) u1) (CHead e1
 261 (Bind b1) v1))).(\lambda (H3: (eq C (CHead c0 (Bind b) u2) c2)).((let H4 \def
 262 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
 263 [(CSort _) \Rightarrow u1 | (CHead _ _ t) \Rightarrow t])) (CHead c1 (Bind
 264 Void) u1) (CHead e1 (Bind b1) v1) H2) in ((let H5 \def (f_equal C B (\lambda
 265 (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow
 266 Void | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
 267 [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Void])])) (CHead c1 (Bind
 268 Void) u1) (CHead e1 (Bind b1) v1) H2) in ((let H6 \def (f_equal C C (\lambda
 269 (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1
 270 | (CHead c _ _) \Rightarrow c])) (CHead c1 (Bind Void) u1) (CHead e1 (Bind
 271 b1) v1) H2) in (eq_ind C e1 (\lambda (c: C).((eq B Void b1) \to ((eq T u1 v1)
 272 \to ((eq C (CHead c0 (Bind b) u2) c2) \to ((csub3 g c c0) \to ((not (eq B b
 273 Void)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
 274 T).(eq C c2 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
 275 C).(\lambda (_: T).(csub3 g e1 e2))))))))))) (\lambda (H7: (eq B Void
 276 b1)).(eq_ind B Void (\lambda (_: B).((eq T u1 v1) \to ((eq C (CHead c0 (Bind
 277 b) u2) c2) \to ((csub3 g e1 c0) \to ((not (eq B b Void)) \to (ex2_3 B C T
 278 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
 279 b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1
 280 e2)))))))))) (\lambda (H8: (eq T u1 v1)).(eq_ind T v1 (\lambda (_: T).((eq C
 281 (CHead c0 (Bind b) u2) c2) \to ((csub3 g e1 c0) \to ((not (eq B b Void)) \to
 282 (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
 283 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 284 T).(csub3 g e1 e2))))))))) (\lambda (H9: (eq C (CHead c0 (Bind b) u2)
 285 c2)).(eq_ind C (CHead c0 (Bind b) u2) (\lambda (c: C).((csub3 g e1 c0) \to
 286 ((not (eq B b Void)) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2:
 287 C).(\lambda (v2: T).(eq C c (CHead e2 (Bind b2) v2))))) (\lambda (_:
 288 B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2)))))))) (\lambda (H10:
 289 (csub3 g e1 c0)).(\lambda (_: (not (eq B b Void))).(let H12 \def (eq_ind_r C
 290 c2 (\lambda (c: C).(csub3 g (CHead e1 (Bind b1) v1) c)) H (CHead c0 (Bind b)
 291 u2) H9) in (let H13 \def (eq_ind_r B b1 (\lambda (b0: B).(csub3 g (CHead e1
 292 (Bind b0) v1) (CHead c0 (Bind b) u2))) H12 Void H7) in (ex2_3_intro B C T
 293 (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c0 (Bind b)
 294 u2) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 295 T).(csub3 g e1 e2)))) b c0 u2 (refl_equal C (CHead c0 (Bind b) u2)) H10)))))
 296 c2 H9)) u1 (sym_eq T u1 v1 H8))) b1 H7)) c1 (sym_eq C c1 e1 H6))) H5)) H4))
 297 H3 H0 H1))) | (csub3_abst c1 c0 H0 u t H1) \Rightarrow (\lambda (H2: (eq C
 298 (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1))).(\lambda (H3: (eq C (CHead
 299 c0 (Bind Abbr) u) c2)).((let H4 \def (f_equal C T (\lambda (e: C).(match e in
 300 C return (\lambda (_: C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t0)
 301 \Rightarrow t0])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H2) in
 302 ((let H5 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
 303 C).B) with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k
 304 in K return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _)
 305 \Rightarrow Abst])])) (CHead c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H2) in
 306 ((let H6 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_:
 307 C).C) with [(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) (CHead
 308 c1 (Bind Abst) t) (CHead e1 (Bind b1) v1) H2) in (eq_ind C e1 (\lambda (c:
 309 C).((eq B Abst b1) \to ((eq T t v1) \to ((eq C (CHead c0 (Bind Abbr) u) c2)
 310 \to ((csub3 g c c0) \to ((ty3 g c0 u t) \to (ex2_3 B C T (\lambda (b2:
 311 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind b2) v2)))))
 312 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2)))))))))))
 313 (\lambda (H7: (eq B Abst b1)).(eq_ind B Abst (\lambda (_: B).((eq T t v1) \to
 314 ((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g e1 c0) \to ((ty3 g c0 u t)
 315 \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C c2
 316 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_:
 317 T).(csub3 g e1 e2)))))))))) (\lambda (H8: (eq T t v1)).(eq_ind T v1 (\lambda
 318 (t0: T).((eq C (CHead c0 (Bind Abbr) u) c2) \to ((csub3 g e1 c0) \to ((ty3 g
 319 c0 u t0) \to (ex2_3 B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
 320 T).(eq C c2 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
 321 C).(\lambda (_: T).(csub3 g e1 e2))))))))) (\lambda (H9: (eq C (CHead c0
 322 (Bind Abbr) u) c2)).(eq_ind C (CHead c0 (Bind Abbr) u) (\lambda (c:
 323 C).((csub3 g e1 c0) \to ((ty3 g c0 u v1) \to (ex2_3 B C T (\lambda (b2:
 324 B).(\lambda (e2: C).(\lambda (v2: T).(eq C c (CHead e2 (Bind b2) v2)))))
 325 (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csub3 g e1 e2))))))))
 326 (\lambda (H10: (csub3 g e1 c0)).(\lambda (_: (ty3 g c0 u v1)).(let H12 \def
 327 (eq_ind_r C c2 (\lambda (c: C).(csub3 g (CHead e1 (Bind b1) v1) c)) H (CHead
 328 c0 (Bind Abbr) u) H9) in (let H13 \def (eq_ind_r B b1 (\lambda (b: B).(csub3
 329 g (CHead e1 (Bind b) v1) (CHead c0 (Bind Abbr) u))) H12 Abst H7) in
 330 (ex2_3_intro B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C
 331 (CHead c0 (Bind Abbr) u) (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda
 332 (e2: C).(\lambda (_: T).(csub3 g e1 e2)))) Abbr c0 u (refl_equal C (CHead c0
 333 (Bind Abbr) u)) H10))))) c2 H9)) t (sym_eq T t v1 H8))) b1 H7)) c1 (sym_eq C
 334 c1 e1 H6))) H5)) H4)) H3 H0 H1)))]) in (H0 (refl_equal C (CHead e1 (Bind b1)
 335 v1)) (refl_equal C c2)))))))).
 336