helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd".
  18
  19 include "iso/defs.ma".
  20
  21 theorem iso_flats_lref_bind_false:
  22  \forall (f: F).(\forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall
  23 (t: T).(\forall (vs: TList).((iso (THeads (Flat f) vs (TLRef i)) (THead (Bind
  24 b) v t)) \to (\forall (P: Prop).P)))))))
  25 \def
  26  \lambda (f: F).(\lambda (b: B).(\lambda (i: nat).(\lambda (v: T).(\lambda
  27 (t: T).(\lambda (vs: TList).(TList_ind (\lambda (t0: TList).((iso (THeads
  28 (Flat f) t0 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P: Prop).P)))
  29 (\lambda (H: (iso (TLRef i) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0
  30 \def (match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_:
  31 (iso t0 t1)).((eq T t0 (TLRef i)) \to ((eq T t1 (THead (Bind b) v t)) \to
  32 P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1)
  33 (TLRef i))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v t))).((let H2
  34 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
  35 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
  36 (THead _ _ _) \Rightarrow False])) I (TLRef i) H0) in (False_ind ((eq T
  37 (TSort n2) (THead (Bind b) v t)) \to P) H2)) H1))) | (iso_lref i1 i2)
  38 \Rightarrow (\lambda (H0: (eq T (TLRef i1) (TLRef i))).(\lambda (H1: (eq T
  39 (TLRef i2) (THead (Bind b) v t))).((let H2 \def (f_equal T nat (\lambda (e:
  40 T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i1 |
  41 (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i1])) (TLRef i1) (TLRef
  42 i) H0) in (eq_ind nat i (\lambda (_: nat).((eq T (TLRef i2) (THead (Bind b) v
  43 t)) \to P)) (\lambda (H3: (eq T (TLRef i2) (THead (Bind b) v t))).(let H4
  44 \def (eq_ind T (TLRef i2) (\lambda (e: T).(match e in T return (\lambda (_:
  45 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
  46 (THead _ _ _) \Rightarrow False])) I (THead (Bind b) v t) H3) in (False_ind P
  47 H4))) i1 (sym_eq nat i1 i H2))) H1))) | (iso_head k v1 v2 t1 t2) \Rightarrow
  48 (\lambda (H0: (eq T (THead k v1 t1) (TLRef i))).(\lambda (H1: (eq T (THead k
  49 v2 t2) (THead (Bind b) v t))).((let H2 \def (eq_ind T (THead k v1 t1)
  50 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
  51 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
  52 True])) I (TLRef i) H0) in (False_ind ((eq T (THead k v2 t2) (THead (Bind b)
  53 v t)) \to P) H2)) H1)))]) in (H0 (refl_equal T (TLRef i)) (refl_equal T
  54 (THead (Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_:
  55 (((iso (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P:
  56 Prop).P)))).(\lambda (H0: (iso (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef
  57 i))) (THead (Bind b) v t))).(\lambda (P: Prop).(let H1 \def (match H0 in iso
  58 return (\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (iso t2 t3)).((eq T t2
  59 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) \to ((eq T t3 (THead
  60 (Bind b) v t)) \to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H1:
  61 (eq T (TSort n1) (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef
  62 i))))).(\lambda (H2: (eq T (TSort n2) (THead (Bind b) v t))).((let H3 \def
  63 (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
  64 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
  65 (THead _ _ _) \Rightarrow False])) I (THead (Flat f) t0 (THeads (Flat f) t1
  66 (TLRef i))) H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P)
  67 H3)) H2))) | (iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1)
  68 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T
  69 (TLRef i2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TLRef i1) (\lambda
  70 (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
  71 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
  72 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in (False_ind ((eq T
  73 (TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) | (iso_head k v1 v2 t2 t3)
  74 \Rightarrow (\lambda (H1: (eq T (THead k v1 t2) (THead (Flat f) t0 (THeads
  75 (Flat f) t1 (TLRef i))))).(\lambda (H2: (eq T (THead k v2 t3) (THead (Bind b)
  76 v t))).((let H3 \def (f_equal T T (\lambda (e: T).(match e in T return
  77 (\lambda (_: T).T) with [(TSort _) \Rightarrow t2 | (TLRef _) \Rightarrow t2
  78 | (THead _ _ t) \Rightarrow t])) (THead k v1 t2) (THead (Flat f) t0 (THeads
  79 (Flat f) t1 (TLRef i))) H1) in ((let H4 \def (f_equal T T (\lambda (e:
  80 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 |
  81 (TLRef _) \Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead k v1 t2)
  82 (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))) H1) in ((let H5 \def
  83 (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with
  84 [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _)
  85 \Rightarrow k])) (THead k v1 t2) (THead (Flat f) t0 (THeads (Flat f) t1
  86 (TLRef i))) H1) in (eq_ind K (Flat f) (\lambda (k0: K).((eq T v1 t0) \to ((eq
  87 T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead k0 v2 t3) (THead (Bind
  88 b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0 (\lambda (_:
  89 T).((eq T t2 (THeads (Flat f) t1 (TLRef i))) \to ((eq T (THead (Flat f) v2
  90 t3) (THead (Bind b) v t)) \to P))) (\lambda (H7: (eq T t2 (THeads (Flat f) t1
  91 (TLRef i)))).(eq_ind T (THeads (Flat f) t1 (TLRef i)) (\lambda (_: T).((eq T
  92 (THead (Flat f) v2 t3) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T
  93 (THead (Flat f) v2 t3) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead
  94 (Flat f) v2 t3) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop)
  95 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _
  96 _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
  97 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8)
  98 in (False_ind P H9))) t2 (sym_eq T t2 (THeads (Flat f) t1 (TLRef i)) H7))) v1
  99 (sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f) H5))) H4)) H3)) H2)))]) in (H1
 100 (refl_equal T (THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i)))) (refl_equal
 101 T (THead (Bind b) v t))))))))) vs)))))).
 102
 103 theorem iso_flats_flat_bind_false:
 104  \forall (f1: F).(\forall (f2: F).(\forall (b: B).(\forall (v: T).(\forall
 105 (v2: T).(\forall (t: T).(\forall (t2: T).(\forall (vs: TList).((iso (THeads
 106 (Flat f1) vs (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to (\forall (P:
 107 Prop).P)))))))))
 108 \def
 109  \lambda (f1: F).(\lambda (f2: F).(\lambda (b: B).(\lambda (v: T).(\lambda
 110 (v2: T).(\lambda (t: T).(\lambda (t2: T).(\lambda (vs: TList).(TList_ind
 111 (\lambda (t0: TList).((iso (THeads (Flat f1) t0 (THead (Flat f2) v2 t2))
 112 (THead (Bind b) v t)) \to (\forall (P: Prop).P))) (\lambda (H: (iso (THead
 113 (Flat f2) v2 t2) (THead (Bind b) v t))).(\lambda (P: Prop).(let H0 \def
 114 (match H in iso return (\lambda (t0: T).(\lambda (t1: T).(\lambda (_: (iso t0
 115 t1)).((eq T t0 (THead (Flat f2) v2 t2)) \to ((eq T t1 (THead (Bind b) v t))
 116 \to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H0: (eq T (TSort n1)
 117 (THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (TSort n2) (THead (Bind b) v
 118 t))).((let H2 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return
 119 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
 120 \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat f2) v2
 121 t2) H0) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H2))
 122 H1))) | (iso_lref i1 i2) \Rightarrow (\lambda (H0: (eq T (TLRef i1) (THead
 123 (Flat f2) v2 t2))).(\lambda (H1: (eq T (TLRef i2) (THead (Bind b) v
 124 t))).((let H2 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T return
 125 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 126 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat f2) v2
 127 t2) H0) in (False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H2))
 128 H1))) | (iso_head k v1 v0 t1 t0) \Rightarrow (\lambda (H0: (eq T (THead k v1
 129 t1) (THead (Flat f2) v2 t2))).(\lambda (H1: (eq T (THead k v0 t0) (THead
 130 (Bind b) v t))).((let H2 \def (f_equal T T (\lambda (e: T).(match e in T
 131 return (\lambda (_: T).T) with [(TSort _) \Rightarrow t1 | (TLRef _)
 132 \Rightarrow t1 | (THead _ _ t) \Rightarrow t])) (THead k v1 t1) (THead (Flat
 133 f2) v2 t2) H0) in ((let H3 \def (f_equal T T (\lambda (e: T).(match e in T
 134 return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _)
 135 \Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead k v1 t1) (THead (Flat
 136 f2) v2 t2) H0) in ((let H4 \def (f_equal T K (\lambda (e: T).(match e in T
 137 return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
 138 \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k v1 t1) (THead (Flat
 139 f2) v2 t2) H0) in (eq_ind K (Flat f2) (\lambda (k0: K).((eq T v1 v2) \to ((eq
 140 T t1 t2) \to ((eq T (THead k0 v0 t0) (THead (Bind b) v t)) \to P)))) (\lambda
 141 (H5: (eq T v1 v2)).(eq_ind T v2 (\lambda (_: T).((eq T t1 t2) \to ((eq T
 142 (THead (Flat f2) v0 t0) (THead (Bind b) v t)) \to P))) (\lambda (H6: (eq T t1
 143 t2)).(eq_ind T t2 (\lambda (_: T).((eq T (THead (Flat f2) v0 t0) (THead (Bind
 144 b) v t)) \to P)) (\lambda (H7: (eq T (THead (Flat f2) v0 t0) (THead (Bind b)
 145 v t))).(let H8 \def (eq_ind T (THead (Flat f2) v0 t0) (\lambda (e: T).(match
 146 e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
 147 (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
 148 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
 149 True])])) I (THead (Bind b) v t) H7) in (False_ind P H8))) t1 (sym_eq T t1 t2
 150 H6))) v1 (sym_eq T v1 v2 H5))) k (sym_eq K k (Flat f2) H4))) H3)) H2))
 151 H1)))]) in (H0 (refl_equal T (THead (Flat f2) v2 t2)) (refl_equal T (THead
 152 (Bind b) v t)))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_: (((iso
 153 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to
 154 (\forall (P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f1) t0 (THeads (Flat
 155 f1) t1 (THead (Flat f2) v2 t2))) (THead (Bind b) v t))).(\lambda (P:
 156 Prop).(let H1 \def (match H0 in iso return (\lambda (t3: T).(\lambda (t4:
 157 T).(\lambda (_: (iso t3 t4)).((eq T t3 (THead (Flat f1) t0 (THeads (Flat f1)
 158 t1 (THead (Flat f2) v2 t2)))) \to ((eq T t4 (THead (Bind b) v t)) \to P)))))
 159 with [(iso_sort n1 n2) \Rightarrow (\lambda (H1: (eq T (TSort n1) (THead
 160 (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2:
 161 (eq T (TSort n2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TSort n1)
 162 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
 163 \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
 164 False])) I (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))
 165 H1) in (False_ind ((eq T (TSort n2) (THead (Bind b) v t)) \to P) H3)) H2))) |
 166 (iso_lref i1 i2) \Rightarrow (\lambda (H1: (eq T (TLRef i1) (THead (Flat f1)
 167 t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda (H2: (eq T
 168 (TLRef i2) (THead (Bind b) v t))).((let H3 \def (eq_ind T (TLRef i1) (\lambda
 169 (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 170 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
 171 (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in
 172 (False_ind ((eq T (TLRef i2) (THead (Bind b) v t)) \to P) H3)) H2))) |
 173 (iso_head k v1 v0 t3 t4) \Rightarrow (\lambda (H1: (eq T (THead k v1 t3)
 174 (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))))).(\lambda
 175 (H2: (eq T (THead k v0 t4) (THead (Bind b) v t))).((let H3 \def (f_equal T T
 176 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
 177 \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ _ t) \Rightarrow t]))
 178 (THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
 179 t2))) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e in T return
 180 (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1
 181 | (THead _ t _) \Rightarrow t])) (THead k v1 t3) (THead (Flat f1) t0 (THeads
 182 (Flat f1) t1 (THead (Flat f2) v2 t2))) H1) in ((let H5 \def (f_equal T K
 183 (\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _)
 184 \Rightarrow k | (TLRef _) \Rightarrow k | (THead k _ _) \Rightarrow k]))
 185 (THead k v1 t3) (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
 186 t2))) H1) in (eq_ind K (Flat f1) (\lambda (k0: K).((eq T v1 t0) \to ((eq T t3
 187 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to ((eq T (THead k0 v0 t4)
 188 (THead (Bind b) v t)) \to P)))) (\lambda (H6: (eq T v1 t0)).(eq_ind T t0
 189 (\lambda (_: T).((eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) \to
 190 ((eq T (THead (Flat f1) v0 t4) (THead (Bind b) v t)) \to P))) (\lambda (H7:
 191 (eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)))).(eq_ind T (THeads
 192 (Flat f1) t1 (THead (Flat f2) v2 t2)) (\lambda (_: T).((eq T (THead (Flat f1)
 193 v0 t4) (THead (Bind b) v t)) \to P)) (\lambda (H8: (eq T (THead (Flat f1) v0
 194 t4) (THead (Bind b) v t))).(let H9 \def (eq_ind T (THead (Flat f1) v0 t4)
 195 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
 196 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
 197 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False |
 198 (Flat _) \Rightarrow True])])) I (THead (Bind b) v t) H8) in (False_ind P
 199 H9))) t3 (sym_eq T t3 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) H7))) v1
 200 (sym_eq T v1 t0 H6))) k (sym_eq K k (Flat f1) H5))) H4)) H3)) H2)))]) in (H1
 201 (refl_equal T (THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2
 202 t2)))) (refl_equal T (THead (Bind b) v t))))))))) vs)))))))).
 203