matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/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
  18
  19 include "iso/defs.ma".
  20
  21 include "tlist/defs.ma".
  22
  23 theorem iso_flats_lref_bind_false:
  24  \forall (f: F).(\forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall
  25 (t: T).(\forall (vs: TList).((iso (THeads (Flat f) vs (TLRef i)) (THead (Bind
  26 b) v t)) \to (\forall (P: Prop).P)))))))
  27 \def
  28  \lambda (f: F).(\lambda (b: B).(\lambda (i: nat).(\lambda (v: T).(\lambda
  29 (t: T).(\lambda (vs: TList).(TList_ind (\lambda (t0: TList).((iso (THeads
  30 (Flat f) t0 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P: Prop).P)))
  31 (\lambda (H: (iso (TLRef i) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0
  32 \def (match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_:
  33 (iso t0 t1)).((eq T t0 (TLRef i)) \to ((eq T t1 (THead (Bind b) v t)) \to
  34 P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1)
  35 (TLRef i))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v t))).((let H2
  36 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
  37 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
  38 (THead _ _ _) \Rightarrow False])) I (TLRef i) H0) in (False_ind ((eq T
  39 (TSort n2) (THead (Bind b) v t)) \to P) H2)) H1))) | (iso_lref i1 i2)
  40 \Rightarrow (\lambda (H0: (eq T (TLRef i1) (TLRef i))).(\lambda (H1: (eq T
  41 (TLRef i2) (THead (Bind b) v t))).((let H2 \def (f_equal T nat (\lambda (e:
  42 T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i1 |
  43 (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i1])) (TLRef i1) (TLRef
  44 i) H0) in (eq_ind nat i (\lambda (_: nat).((eq T (TLRef i2) (THead (Bind b) v
  45 t)) \to P)) (\lambda (H3: (eq T (TLRef i2) (THead (Bind b) v t))).(let H4
  46 \def (eq_ind T (TLRef i2) (\lambda (e: T).(match e in T return (\lambda (_:
  47 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
  48 (THead _ _ _) \Rightarrow False])) I (THead (Bind b) v t) H3) in (False_ind P
  49 H4))) i1 (sym_eq nat i1 i H2))) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow
  50 (\lambda (H0: (eq T (THead k v1 t1) (TLRef i))).(\lambda (H1: (eq T (THead k
  51 v2 t2) (THead (Bind b) v t))).((let H2 \def (eq_ind T (THead k v1 t1)
  52 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
  53 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
  54 True])) I (TLRef i) H0) in (False_ind ((eq T (THead k v2 t2) (THead (Bind b)
  55 v t)) \to P) H2)) H1)))]) in (H0 (refl_equal T (TLRef i)) (refl_equal T
  56 (THead (Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_:
  57 (((iso (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P:
  58 Prop).P)))).(\lambda (H0: (iso (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef
  59 i))) (THead (Bind b) v t))).(\lambda (P: Prop).(let H1 \def (match H0 in iso
  60 return (\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (iso t2 t3)).((eq T t2
  61 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) \to ((eq T t3 (THead
  62 (Bind b) v t)) \to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H1:
  63 (eq T (TSort n1) (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef
  64 i))))).(\lambda (H2: (eq T (TSort n2) (THead (Bind b) v t))).((let H3 \def
  65 (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
  66 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
  67 (THead _ _ _) \Rightarrow False])) I (THead (Flat f) t0 (THeads (Flat f) t1
  68 (TLRef i))) H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P)
  69 H3)) H2))) | (iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1)
  70 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T
  71 (TLRef i2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TLRef i1) (\lambda
  72 (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
  73 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
  74 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in (False_ind ((eq T
  75 (TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) | (iso_head v1 v2 t2 t3 k)
  76 \Rightarrow (\lambda (H1: (eq T (THead k v1 t2) (THead (Flat f) t0 (THeads
  77 (Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T (THead k v2 t3) (THead (Bind b)
  78 v t))).((let H3 \def (f_equal T T (\lambda (e: T).(match e in T return
  79 (\lambda (_: T).T) with [(TSort _) \Rightarrow t2 | (TLRef _) \Rightarrow t2
  80 | (THead _ _ t4) \Rightarrow t4])) (THead k v1 t2) (THead (Flat f) t0 (THeads
  81 (Flat f) t1 (TLRef i))) H1) in ((let H4 \def (f_equal T T (\lambda (e:
  82 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 |
  83 (TLRef _) \Rightarrow v1 | (THead _ t4 _) \Rightarrow t4])) (THead k v1 t2)
  84 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in ((let H5 \def
  85 (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with
  86 [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
  87 \Rightarrow k0])) (THead k v1 t2) (THead (Flat f) t0 (THeads (Flat f) t1
  88 (TLRef i))) H1) in (eq_ind K (Flat f) (\lambda (k0: K).((eq T v1 t0) \to ((eq
  89 T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead k0 v2 t3) (THead (Bind
  90 b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0 (\lambda (_:
  91 T).((eq T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead (Flat f) v2
  92 t3) (THead (Bind b) v t)) \to P))) (\lambda (H7: (eq T t2 (THeads (Flat f) t1
  93 (TLRef i)))).(eq_ind T (THeads (Flat f) t1 (TLRef i)) (\lambda (_: T).((eq T
  94 (THead (Flat f) v2 t3) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T
  95 (THead (Flat f) v2 t3) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead
  96 (Flat f) v2 t3) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop)
  97 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k0 _
  98 _) \Rightarrow (match k0 in K return (\lambda (_: K).Prop) with [(Bind _)
  99 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8)
 100 in (False_ind P H9))) t2 (sym_eq T t2 (THeads (Flat f) t1 (TLRef i)) H7))) v1
 101 (sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f) H5))) H4)) H3)) H2)))]) in (H1
 102 (refl_equal T (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) (refl_equal
 103 T (THead (Bind b) v t))))))))) vs)))))).
 104
 105 theorem iso_flats_flat_bind_false:
 106  \forall (f1: F).(\forall (f2: F).(\forall (b: B).(\forall (v: T).(\forall
 107 (v2: T).(\forall (t: T).(\forall (t2: T).(\forall (vs: TList).((iso (THeads
 108 (Flat f1) vs (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to (\forall (P:
 109 Prop).P)))))))))
 110 \def
 111  \lambda (f1: F).(\lambda (f2: F).(\lambda (b: B).(\lambda (v: T).(\lambda
 112 (v2: T).(\lambda (t: T).(\lambda (t2: T).(\lambda (vs: TList).(TList_ind
 113 (\lambda (t0: TList).((iso (THeads (Flat f1) t0 (THead (Flat f2) v2 t2))
 114 (THead (Bind b) v t)) \to (\forall (P: Prop).P))) (\lambda (H: (iso (THead
 115 (Flat f2) v2 t2) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0 \def
 116 (match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_: (iso t0
 117 t1)).((eq T t0 (THead (Flat f2) v2 t2)) \to ((eq T t1 (THead (Bind b) v t))
 118 \to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1)
 119 (THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v
 120 t))).((let H2 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return
 121 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
 122 \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat f2) v2
 123 t2) H0) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H2))
 124 H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: (eq T (TLRef i1) (THead
 125 (Flat f2) v2 t2))).(\lambda (H1: (eq T (TLRef i2) (THead (Bind b) v
 126 t))).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return
 127 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 128 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat f2) v2
 129 t2) H0) in (False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H2))
 130 H1))) | (iso_head v1 v0 t1 t0 k) \Rightarrow (\lambda (H0: (eq T (THead k v1
 131 t1) (THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (THead k v0 t0) (THead
 132 (Bind b) v t))).((let H2 \def (f_equal T T (\lambda (e: T).(match e in T
 133 return (\lambda (_: T).T) with [(TSort _) \Rightarrow t1 | (TLRef _)
 134 \Rightarrow t1 | (THead _ _ t3) \Rightarrow t3])) (THead k v1 t1) (THead
 135 (Flat f2) v2 t2) H0) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e
 136 in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _)
 137 \Rightarrow v1 | (THead _ t3 _) \Rightarrow t3])) (THead k v1 t1) (THead
 138 (Flat f2) v2 t2) H0) in ((let H4 \def (f_equal T K (\lambda (e: T).(match e
 139 in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
 140 \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k v1 t1) (THead (Flat
 141 f2) v2 t2) H0) in (eq_ind K (Flat f2) (\lambda (k0: K).((eq T v1 v2) \to ((eq
 142 T t1 t2) \to ((eq T (THead k0 v0 t0) (THead (Bind b) v t)) \to P)))) (\lambda
 143 (H5: (eq T v1 v2)).(eq_ind T v2 (\lambda (_: T).((eq T t1 t2) \to ((eq T
 144 (THead (Flat f2) v0 t0) (THead (Bind b) v t)) \to P))) (\lambda (H6: (eq T t1
 145 t2)).(eq_ind T t2 (\lambda (_: T).((eq T (THead (Flat f2) v0 t0) (THead (Bind
 146 b) v t)) \to P)) (\lambda (H7: (eq T (THead (Flat f2) v0 t0) (THead (Bind b)
 147 v t))).(let H8 \def (eq_ind T (THead (Flat f2) v0 t0) (\lambda (e: T).(match
 148 e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
 149 (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K
 150 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _)
 151 \Rightarrow True])])) I (THead (Bind b) v t) H7) in (False_ind P H8))) t1
 152 (sym_eq T t1 t2 H6))) v1 (sym_eq T v1 v2 H5))) k (sym_eq K k (Flat f2) H4)))
 153 H3)) H2)) H1)))]) in (H0 (refl_equal T (THead (Flat f2) v2 t2)) (refl_equal T
 154 (THead (Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_:
 155 (((iso (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t))
 156 \to (\forall (P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f1) t0 (THeads
 157 (Flat f1) t1 (THead (Flat f2) v2 t2))) (THead (Bind b) v t))).(\lambda (P:
 158 Prop).(let H1 \def (match H0 in iso return (\lambda (t3: T).(\lambda (t4:
 159 T).(\lambda (_: (iso t3 t4)).((eq T t3 (THead (Flat f1) t0 (THeads (Flat f1)
 160 t1 (THead (Flat f2) v2 t2)))) \to ((eq T t4 (THead (Bind b) v t)) \to P)))))
 161 with [(iso_sort n1 n2) \Rightarrow (\lambda (H1: (eq T (TSort n1) (THead
 162 (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2:
 163 (eq T (TSort n2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TSort n1)
 164 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
 165 \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
 166 False])) I (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))
 167 H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H3)) H2))) |
 168 (iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1) (THead (Flat f1)
 169 t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2: (eq T
 170 (TLRef i2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TLRef i1) (\lambda
 171 (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 172 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
 173 (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in
 174 (False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) |
 175 (iso_head v1 v0 t3 t4 k) \Rightarrow (\lambda (H1: (eq T (THead k v1 t3)
 176 (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda
 177 (H2: (eq T (THead k v0 t4) (THead (Bind b) v t))).((let H3 \def (f_equal T T
 178 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
 179 \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t5) \Rightarrow t5]))
 180 (THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
 181 t2))) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e in T return
 182 (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1
 183 | (THead _ t5 _) \Rightarrow t5])) (THead k v1 t3) (THead (Flat f1) t0
 184 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in ((let H5 \def (f_equal
 185 T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _)
 186 \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0]))
 187 (THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
 188 t2))) H1) in (eq_ind K (Flat f1) (\lambda (k0: K).((eq T v1 t0) \to ((eq T t3
 189 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to ((eq T (THead k0 v0 t4)
 190 (THead (Bind b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0
 191 (\lambda (_: T).((eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to
 192 ((eq T (THead (Flat f1) v0 t4) (THead (Bind b) v t)) \to P))) (\lambda (H7:
 193 (eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))).(eq_ind T (THeads
 194 (Flat f1) t1 (THead (Flat f2) v2 t2)) (\lambda (_: T).((eq T (THead (Flat f1)
 195 v0 t4) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T (THead (Flat f1) v0
 196 t4) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead (Flat f1) v0 t4)
 197 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
 198 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow
 199 (match k0 in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False
 200 | (Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8) in (False_ind P
 201 H9))) t3 (sym_eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) H7))) v1
 202 (sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f1) H5))) H4)) H3)) H2)))]) in (H1
 203 (refl_equal T (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
 204 t2)))) (refl_equal T (THead (Bind b) v t))))))))) vs)))))))).
 205
 206 theorem iso_gen_sort:
 207  \forall (u2: T).(\forall (n1: nat).((iso (TSort n1) u2) \to (ex nat (\lambda
 208 (n2: nat).(eq T u2 (TSort n2))))))
 209 \def
 210  \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TSort n1) u2)).(let H0
 211 \def (match H in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_:
 212 (iso t t0)).((eq T t (TSort n1)) \to ((eq T t0 u2) \to (ex nat (\lambda (n2:
 213 nat).(eq T u2 (TSort n2))))))))) with [(iso_sort n0 n2) \Rightarrow (\lambda
 214 (H0: (eq T (TSort n0) (TSort n1))).(\lambda (H1: (eq T (TSort n2) u2)).((let
 215 H2 \def (f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_:
 216 T).nat) with [(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _
 217 _) \Rightarrow n0])) (TSort n0) (TSort n1) H0) in (eq_ind nat n1 (\lambda (_:
 218 nat).((eq T (TSort n2) u2) \to (ex nat (\lambda (n3: nat).(eq T u2 (TSort
 219 n3)))))) (\lambda (H3: (eq T (TSort n2) u2)).(eq_ind T (TSort n2) (\lambda
 220 (t: T).(ex nat (\lambda (n3: nat).(eq T t (TSort n3))))) (ex_intro nat
 221 (\lambda (n3: nat).(eq T (TSort n2) (TSort n3))) n2 (refl_equal T (TSort
 222 n2))) u2 H3)) n0 (sym_eq nat n0 n1 H2))) H1))) | (iso_lref i1 i2) \Rightarrow
 223 (\lambda (H0: (eq T (TLRef i1) (TSort n1))).(\lambda (H1: (eq T (TLRef i2)
 224 u2)).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return
 225 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 226 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n1) H0) in
 227 (False_ind ((eq T (TLRef i2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2
 228 (TSort n2))))) H2)) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow (\lambda
 229 (H0: (eq T (THead k v1 t1) (TSort n1))).(\lambda (H1: (eq T (THead k v2 t2)
 230 u2)).((let H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T
 231 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 232 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n1) H0) in
 233 (False_ind ((eq T (THead k v2 t2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2
 234 (TSort n2))))) H2)) H1)))]) in (H0 (refl_equal T (TSort n1)) (refl_equal T
 235 u2))))).
 236
 237 theorem iso_gen_lref:
 238  \forall (u2: T).(\forall (n1: nat).((iso (TLRef n1) u2) \to (ex nat (\lambda
 239 (n2: nat).(eq T u2 (TLRef n2))))))
 240 \def
 241  \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TLRef n1) u2)).(let H0
 242 \def (match H in iso return (\lambda (t: T).(\lambda (t0: T).(\lambda (_:
 243 (iso t t0)).((eq T t (TLRef n1)) \to ((eq T t0 u2) \to (ex nat (\lambda (n2:
 244 nat).(eq T u2 (TLRef n2))))))))) with [(iso_sort n0 n2) \Rightarrow (\lambda
 245 (H0: (eq T (TSort n0) (TLRef n1))).(\lambda (H1: (eq T (TSort n2) u2)).((let
 246 H2 \def (eq_ind T (TSort n0) (\lambda (e: T).(match e in T return (\lambda
 247 (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
 248 (THead _ _ _) \Rightarrow False])) I (TLRef n1) H0) in (False_ind ((eq T
 249 (TSort n2) u2) \to (ex nat (\lambda (n3: nat).(eq T u2 (TLRef n3))))) H2))
 250 H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: (eq T (TLRef i1) (TLRef
 251 n1))).(\lambda (H1: (eq T (TLRef i2) u2)).((let H2 \def (f_equal T nat
 252 (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
 253 \Rightarrow i1 | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i1]))
 254 (TLRef i1) (TLRef n1) H0) in (eq_ind nat n1 (\lambda (_: nat).((eq T (TLRef
 255 i2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 (TLRef n2)))))) (\lambda (H3:
 256 (eq T (TLRef i2) u2)).(eq_ind T (TLRef i2) (\lambda (t: T).(ex nat (\lambda
 257 (n2: nat).(eq T t (TLRef n2))))) (ex_intro nat (\lambda (n2: nat).(eq T
 258 (TLRef i2) (TLRef n2))) i2 (refl_equal T (TLRef i2))) u2 H3)) i1 (sym_eq nat
 259 i1 n1 H2))) H1))) | (iso_head v1 v2 t1 t2 k) \Rightarrow (\lambda (H0: (eq T
 260 (THead k v1 t1) (TLRef n1))).(\lambda (H1: (eq T (THead k v2 t2) u2)).((let
 261 H2 \def (eq_ind T (THead k v1 t1) (\lambda (e: T).(match e in T return
 262 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 263 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n1) H0) in
 264 (False_ind ((eq T (THead k v2 t2) u2) \to (ex nat (\lambda (n2: nat).(eq T u2
 265 (TLRef n2))))) H2)) H1)))]) in (H0 (refl_equal T (TLRef n1)) (refl_equal T
 266 u2))))).
 267
 268 theorem iso_gen_head:
 269  \forall (k: K).(\forall (v1: T).(\forall (t1: T).(\forall (u2: T).((iso
 270 (THead k v1 t1) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2
 271 (THead k v2 t2)))))))))
 272 \def
 273  \lambda (k: K).(\lambda (v1: T).(\lambda (t1: T).(\lambda (u2: T).(\lambda
 274 (H: (iso (THead k v1 t1) u2)).(let H0 \def (match H in iso return (\lambda
 275 (t: T).(\lambda (t0: T).(\lambda (_: (iso t t0)).((eq T t (THead k v1 t1))
 276 \to ((eq T t0 u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2
 277 (THead k v2 t2)))))))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq
 278 T (TSort n1) (THead k v1 t1))).(\lambda (H1: (eq T (TSort n2) u2)).((let H2
 279 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
 280 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
 281 (THead _ _ _) \Rightarrow False])) I (THead k v1 t1) H0) in (False_ind ((eq T
 282 (TSort n2) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2
 283 (THead k v2 t2)))))) H2)) H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0:
 284 (eq T (TLRef i1) (THead k v1 t1))).(\lambda (H1: (eq T (TLRef i2) u2)).((let
 285 H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return (\lambda
 286 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
 287 (THead _ _ _) \Rightarrow False])) I (THead k v1 t1) H0) in (False_ind ((eq T
 288 (TLRef i2) u2) \to (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T u2
 289 (THead k v2 t2)))))) H2)) H1))) | (iso_head v0 v2 t0 t2 k0) \Rightarrow
 290 (\lambda (H0: (eq T (THead k0 v0 t0) (THead k v1 t1))).(\lambda (H1: (eq T
 291 (THead k0 v2 t2) u2)).((let H2 \def (f_equal T T (\lambda (e: T).(match e in
 292 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
 293 \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k0 v0 t0) (THead k v1
 294 t1) H0) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e in T return
 295 (\lambda (_: T).T) with [(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0
 296 | (THead _ t _) \Rightarrow t])) (THead k0 v0 t0) (THead k v1 t1) H0) in
 297 ((let H4 \def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_:
 298 T).K) with [(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k1 _
 299 _) \Rightarrow k1])) (THead k0 v0 t0) (THead k v1 t1) H0) in (eq_ind K k
 300 (\lambda (k1: K).((eq T v0 v1) \to ((eq T t0 t1) \to ((eq T (THead k1 v2 t2)
 301 u2) \to (ex_2 T T (\lambda (v3: T).(\lambda (t3: T).(eq T u2 (THead k v3
 302 t3))))))))) (\lambda (H5: (eq T v0 v1)).(eq_ind T v1 (\lambda (_: T).((eq T
 303 t0 t1) \to ((eq T (THead k v2 t2) u2) \to (ex_2 T T (\lambda (v3: T).(\lambda
 304 (t3: T).(eq T u2 (THead k v3 t3)))))))) (\lambda (H6: (eq T t0 t1)).(eq_ind T
 305 t1 (\lambda (_: T).((eq T (THead k v2 t2) u2) \to (ex_2 T T (\lambda (v3:
 306 T).(\lambda (t3: T).(eq T u2 (THead k v3 t3))))))) (\lambda (H7: (eq T (THead
 307 k v2 t2) u2)).(eq_ind T (THead k v2 t2) (\lambda (t: T).(ex_2 T T (\lambda
 308 (v3: T).(\lambda (t3: T).(eq T t (THead k v3 t3)))))) (ex_2_intro T T
 309 (\lambda (v3: T).(\lambda (t3: T).(eq T (THead k v2 t2) (THead k v3 t3)))) v2
 310 t2 (refl_equal T (THead k v2 t2))) u2 H7)) t0 (sym_eq T t0 t1 H6))) v0
 311 (sym_eq T v0 v1 H5))) k0 (sym_eq K k0 k H4))) H3)) H2)) H1)))]) in (H0
 312 (refl_equal T (THead k v1 t1)) (refl_equal T u2))))))).
 313