matita/matita/contribs/lambdadelta/basic_1A/csubv/clear.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "basic_1A/csubv/fwd.ma".
  18
  19 include "basic_1A/clear/fwd.ma".
  20
  21 lemma csubv_clear_conf:
  22  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1:
  23 B).(\forall (d1: C).(\forall (v1: T).((clear c1 (CHead d1 (Bind b1) v1)) \to
  24 (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
  25 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(clear c2 (CHead d2
  26 (Bind b2) v2))))))))))))
  27 \def
  28  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(csubv_ind
  29 (\lambda (c: C).(\lambda (c0: C).(\forall (b1: B).(\forall (d1: C).(\forall
  30 (v1: T).((clear c (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_:
  31 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
  32 B).(\lambda (d2: C).(\lambda (v2: T).(clear c0 (CHead d2 (Bind b2)
  33 v2)))))))))))) (\lambda (n: nat).(\lambda (b1: B).(\lambda (d1: C).(\lambda
  34 (v1: T).(\lambda (H0: (clear (CSort n) (CHead d1 (Bind b1)
  35 v1))).(clear_gen_sort (CHead d1 (Bind b1) v1) n H0 (ex2_3 B C T (\lambda (_:
  36 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
  37 B).(\lambda (d2: C).(\lambda (v2: T).(clear (CSort n) (CHead d2 (Bind b2)
  38 v2)))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3
  39 c4)).(\lambda (_: ((\forall (b1: B).(\forall (d1: C).(\forall (v1: T).((clear
  40 c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
  41 C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
  42 C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda
  43 (v1: T).(\lambda (v2: T).(\lambda (b1: B).(\lambda (d1: C).(\lambda (v0:
  44 T).(\lambda (H2: (clear (CHead c3 (Bind Void) v1) (CHead d1 (Bind b1)
  45 v0))).(let H3 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
  46 \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind b1) v0)
  47 (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1
  48 H2)) in ((let H4 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
  49 \Rightarrow b1 | (CHead _ k _) \Rightarrow (match k with [(Bind b)
  50 \Rightarrow b | (Flat _) \Rightarrow b1])])) (CHead d1 (Bind b1) v0) (CHead
  51 c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1 H2)) in
  52 ((let H5 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
  53 \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b1) v0)
  54 (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1
  55 H2)) in (\lambda (_: (eq B b1 Void)).(\lambda (H7: (eq C d1 c3)).(eq_ind_r C
  56 c3 (\lambda (c: C).(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
  57 T).(csubv c d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
  58 (CHead c4 (Bind Void) v2) (CHead d2 (Bind b2) v3))))))) (ex2_3_intro B C T
  59 (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda
  60 (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2)
  61 (CHead d2 (Bind b2) v3))))) Void c4 v2 H0 (clear_bind Void c4 v2)) d1 H7))))
  62 H4)) H3)))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3
  63 c4)).(\lambda (_: ((\forall (b1: B).(\forall (d1: C).(\forall (v1: T).((clear
  64 c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
  65 C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
  66 C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda
  67 (b1: B).(\lambda (_: (not (eq B b1 Void))).(\lambda (b2: B).(\lambda (v1:
  68 T).(\lambda (v2: T).(\lambda (b0: B).(\lambda (d1: C).(\lambda (v0:
  69 T).(\lambda (H3: (clear (CHead c3 (Bind b1) v1) (CHead d1 (Bind b0)
  70 v0))).(let H4 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
  71 \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind b0) v0)
  72 (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3))
  73 in ((let H5 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
  74 \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k with [(Bind b)
  75 \Rightarrow b | (Flat _) \Rightarrow b0])])) (CHead d1 (Bind b0) v0) (CHead
  76 c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in
  77 ((let H6 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
  78 \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) v0)
  79 (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3))
  80 in (\lambda (_: (eq B b0 b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3
  81 (\lambda (c: C).(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
  82 T).(csubv c d2)))) (\lambda (b3: B).(\lambda (d2: C).(\lambda (v3: T).(clear
  83 (CHead c4 (Bind b2) v2) (CHead d2 (Bind b3) v3))))))) (ex2_3_intro B C T
  84 (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda
  85 (b3: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind b2) v2)
  86 (CHead d2 (Bind b3) v3))))) b2 c4 v2 H0 (clear_bind b2 c4 v2)) d1 H8)))) H5))
  87 H4))))))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv c3
  88 c4)).(\lambda (H1: ((\forall (b1: B).(\forall (d1: C).(\forall (v1:
  89 T).((clear c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_:
  90 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
  91 B).(\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2)
  92 v2)))))))))))).(\lambda (f1: F).(\lambda (f2: F).(\lambda (v1: T).(\lambda
  93 (v2: T).(\lambda (b1: B).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H2:
  94 (clear (CHead c3 (Flat f1) v1) (CHead d1 (Bind b1) v0))).(let H_x \def (H1 b1
  95 d1 v0 (clear_gen_flat f1 c3 (CHead d1 (Bind b1) v0) v1 H2)) in (let H3 \def
  96 H_x in (ex2_3_ind B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
  97 T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
  98 c4 (CHead d2 (Bind b2) v3))))) (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
  99 C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
 100 C).(\lambda (v3: T).(clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind b2)
 101 v3)))))) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H4:
 102 (csubv d1 x1)).(\lambda (H5: (clear c4 (CHead x1 (Bind x0) x2))).(ex2_3_intro
 103 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))))
 104 (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Flat f2)
 105 v2) (CHead d2 (Bind b2) v3))))) x0 x1 x2 H4 (clear_flat c4 (CHead x1 (Bind
 106 x0) x2) H5 f2 v2))))))) H3))))))))))))))) c1 c2 H))).
 107
 108 lemma csubv_clear_conf_void:
 109  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1:
 110 C).(\forall (v1: T).((clear c1 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T
 111 (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
 112 (v2: T).(clear c2 (CHead d2 (Bind Void) v2))))))))))
 113 \def
 114  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(csubv_ind
 115 (\lambda (c: C).(\lambda (c0: C).(\forall (d1: C).(\forall (v1: T).((clear c
 116 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (_:
 117 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c0 (CHead d2
 118 (Bind Void) v2)))))))))) (\lambda (n: nat).(\lambda (d1: C).(\lambda (v1:
 119 T).(\lambda (H0: (clear (CSort n) (CHead d1 (Bind Void) v1))).(clear_gen_sort
 120 (CHead d1 (Bind Void) v1) n H0 (ex2_2 C T (\lambda (d2: C).(\lambda (_:
 121 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear (CSort n) (CHead
 122 d2 (Bind Void) v2)))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0:
 123 (csubv c3 c4)).(\lambda (_: ((\forall (d1: C).(\forall (v1: T).((clear c3
 124 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (_:
 125 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2
 126 (Bind Void) v2)))))))))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (d1:
 127 C).(\lambda (v0: T).(\lambda (H2: (clear (CHead c3 (Bind Void) v1) (CHead d1
 128 (Bind Void) v0))).(let H3 \def (f_equal C C (\lambda (e: C).(match e with
 129 [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind
 130 Void) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind
 131 Void) v0) v1 H2)) in ((let H4 \def (f_equal C T (\lambda (e: C).(match e with
 132 [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind
 133 Void) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind
 134 Void) v0) v1 H2)) in (\lambda (H5: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c:
 135 C).(ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv c d2))) (\lambda (d2:
 136 C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind Void)
 137 v3)))))) (ex2_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))
 138 (\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2) (CHead d2
 139 (Bind Void) v3)))) c4 v2 H0 (clear_bind Void c4 v2)) d1 H5))) H3)))))))))))
 140 (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv c3 c4)).(\lambda (_:
 141 ((\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1 (Bind Void) v1)) \to
 142 (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2:
 143 C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind Void) v2)))))))))).(\lambda
 144 (b1: B).(\lambda (H2: (not (eq B b1 Void))).(\lambda (b2: B).(\lambda (v1:
 145 T).(\lambda (v2: T).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H3: (clear
 146 (CHead c3 (Bind b1) v1) (CHead d1 (Bind Void) v0))).(let H4 \def (f_equal C C
 147 (\lambda (e: C).(match e with [(CSort _) \Rightarrow d1 | (CHead c _ _)
 148 \Rightarrow c])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
 149 (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1 H3)) in ((let H5 \def
 150 (f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow Void |
 151 (CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
 152 \Rightarrow Void])])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
 153 (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1 H3)) in ((let H6 \def
 154 (f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow v0 | (CHead
 155 _ _ t) \Rightarrow t])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
 156 (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1 H3)) in (\lambda (H7: (eq
 157 B Void b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_2
 158 C T (\lambda (d2: C).(\lambda (_: T).(csubv c d2))) (\lambda (d2: C).(\lambda
 159 (v3: T).(clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)))))) (let H9
 160 \def (eq_ind_r B b1 (\lambda (b: B).(not (eq B b Void))) H2 Void H7) in (let
 161 H10 \def (match (H9 (refl_equal B Void)) in False with []) in H10)) d1 H8))))
 162 H5)) H4)))))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv
 163 c3 c4)).(\lambda (H1: ((\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1
 164 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1
 165 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind Void)
 166 v2)))))))))).(\lambda (f1: F).(\lambda (f2: F).(\lambda (v1: T).(\lambda (v2:
 167 T).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H2: (clear (CHead c3 (Flat f1)
 168 v1) (CHead d1 (Bind Void) v0))).(let H_x \def (H1 d1 v0 (clear_gen_flat f1 c3
 169 (CHead d1 (Bind Void) v0) v1 H2)) in (let H3 \def H_x in (ex2_2_ind C T
 170 (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
 171 (v3: T).(clear c4 (CHead d2 (Bind Void) v3)))) (ex2_2 C T (\lambda (d2:
 172 C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v3: T).(clear
 173 (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3))))) (\lambda (x0:
 174 C).(\lambda (x1: T).(\lambda (H4: (csubv d1 x0)).(\lambda (H5: (clear c4
 175 (CHead x0 (Bind Void) x1))).(ex2_2_intro C T (\lambda (d2: C).(\lambda (_:
 176 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Flat
 177 f2) v2) (CHead d2 (Bind Void) v3)))) x0 x1 H4 (clear_flat c4 (CHead x0 (Bind
 178 Void) x1) H5 f2 v2)))))) H3)))))))))))))) c1 c2 H))).
 179