matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/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 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/clear".
  18
  19 include "csubc/defs.ma".
  20
  21 theorem csubc_clear_conf:
  22  \forall (g: G).(\forall (c1: C).(\forall (e1: C).((clear c1 e1) \to (\forall
  23 (c2: C).((csubc g c1 c2) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda
  24 (e2: C).(csubc g e1 e2))))))))
  25 \def
  26  \lambda (g: G).(\lambda (c1: C).(\lambda (e1: C).(\lambda (H: (clear c1
  27 e1)).(clear_ind (\lambda (c: C).(\lambda (c0: C).(\forall (c2: C).((csubc g c
  28 c2) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g c0
  29 e2))))))) (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(\lambda (c2:
  30 C).(\lambda (H0: (csubc g (CHead e (Bind b) u) c2)).(let H1 \def (match H0 in
  31 csubc return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (csubc ? c
  32 c0)).((eq C c (CHead e (Bind b) u)) \to ((eq C c0 c2) \to (ex2 C (\lambda
  33 (e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g (CHead e (Bind b) u)
  34 e2)))))))) with [(csubc_sort n) \Rightarrow (\lambda (H1: (eq C (CSort n)
  35 (CHead e (Bind b) u))).(\lambda (H2: (eq C (CSort n) c2)).((let H3 \def
  36 (eq_ind C (CSort n) (\lambda (e0: C).(match e0 in C return (\lambda (_:
  37 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
  38 False])) I (CHead e (Bind b) u) H1) in (False_ind ((eq C (CSort n) c2) \to
  39 (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g (CHead e
  40 (Bind b) u) e2)))) H3)) H2))) | (csubc_head c0 c3 H1 k v) \Rightarrow
  41 (\lambda (H2: (eq C (CHead c0 k v) (CHead e (Bind b) u))).(\lambda (H3: (eq C
  42 (CHead c3 k v) c2)).((let H4 \def (f_equal C T (\lambda (e0: C).(match e0 in
  43 C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t)
  44 \Rightarrow t])) (CHead c0 k v) (CHead e (Bind b) u) H2) in ((let H5 \def
  45 (f_equal C K (\lambda (e0: C).(match e0 in C return (\lambda (_: C).K) with
  46 [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) (CHead c0 k v)
  47 (CHead e (Bind b) u) H2) in ((let H6 \def (f_equal C C (\lambda (e0:
  48 C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 |
  49 (CHead c _ _) \Rightarrow c])) (CHead c0 k v) (CHead e (Bind b) u) H2) in
  50 (eq_ind C e (\lambda (c: C).((eq K k (Bind b)) \to ((eq T v u) \to ((eq C
  51 (CHead c3 k v) c2) \to ((csubc g c c3) \to (ex2 C (\lambda (e2: C).(clear c2
  52 e2)) (\lambda (e2: C).(csubc g (CHead e (Bind b) u) e2)))))))) (\lambda (H7:
  53 (eq K k (Bind b))).(eq_ind K (Bind b) (\lambda (k0: K).((eq T v u) \to ((eq C
  54 (CHead c3 k0 v) c2) \to ((csubc g e c3) \to (ex2 C (\lambda (e2: C).(clear c2
  55 e2)) (\lambda (e2: C).(csubc g (CHead e (Bind b) u) e2))))))) (\lambda (H8:
  56 (eq T v u)).(eq_ind T u (\lambda (t: T).((eq C (CHead c3 (Bind b) t) c2) \to
  57 ((csubc g e c3) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2:
  58 C).(csubc g (CHead e (Bind b) u) e2)))))) (\lambda (H9: (eq C (CHead c3 (Bind
  59 b) u) c2)).(eq_ind C (CHead c3 (Bind b) u) (\lambda (c: C).((csubc g e c3)
  60 \to (ex2 C (\lambda (e2: C).(clear c e2)) (\lambda (e2: C).(csubc g (CHead e
  61 (Bind b) u) e2))))) (\lambda (H10: (csubc g e c3)).(ex_intro2 C (\lambda (e2:
  62 C).(clear (CHead c3 (Bind b) u) e2)) (\lambda (e2: C).(csubc g (CHead e (Bind
  63 b) u) e2)) (CHead c3 (Bind b) u) (clear_bind b c3 u) (csubc_head g e c3 H10
  64 (Bind b) u))) c2 H9)) v (sym_eq T v u H8))) k (sym_eq K k (Bind b) H7))) c0
  65 (sym_eq C c0 e H6))) H5)) H4)) H3 H1))) | (csubc_abst c0 c3 H1 v a H2 w H3)
  66 \Rightarrow (\lambda (H4: (eq C (CHead c0 (Bind Abst) v) (CHead e (Bind b)
  67 u))).(\lambda (H5: (eq C (CHead c3 (Bind Abbr) w) c2)).((let H6 \def (f_equal
  68 C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with [(CSort _)
  69 \Rightarrow v | (CHead _ _ t) \Rightarrow t])) (CHead c0 (Bind Abst) v)
  70 (CHead e (Bind b) u) H4) in ((let H7 \def (f_equal C B (\lambda (e0:
  71 C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abst
  72 | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with
  73 [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abst])])) (CHead c0 (Bind
  74 Abst) v) (CHead e (Bind b) u) H4) in ((let H8 \def (f_equal C C (\lambda (e0:
  75 C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 |
  76 (CHead c _ _) \Rightarrow c])) (CHead c0 (Bind Abst) v) (CHead e (Bind b) u)
  77 H4) in (eq_ind C e (\lambda (c: C).((eq B Abst b) \to ((eq T v u) \to ((eq C
  78 (CHead c3 (Bind Abbr) w) c2) \to ((csubc g c c3) \to ((sc3 g (asucc g a) c v)
  79 \to ((sc3 g a c3 w) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2:
  80 C).(csubc g (CHead e (Bind b) u) e2)))))))))) (\lambda (H9: (eq B Abst
  81 b)).(eq_ind B Abst (\lambda (b0: B).((eq T v u) \to ((eq C (CHead c3 (Bind
  82 Abbr) w) c2) \to ((csubc g e c3) \to ((sc3 g (asucc g a) e v) \to ((sc3 g a
  83 c3 w) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g
  84 (CHead e (Bind b0) u) e2))))))))) (\lambda (H10: (eq T v u)).(eq_ind T u
  85 (\lambda (t: T).((eq C (CHead c3 (Bind Abbr) w) c2) \to ((csubc g e c3) \to
  86 ((sc3 g (asucc g a) e t) \to ((sc3 g a c3 w) \to (ex2 C (\lambda (e2:
  87 C).(clear c2 e2)) (\lambda (e2: C).(csubc g (CHead e (Bind Abst) u)
  88 e2)))))))) (\lambda (H11: (eq C (CHead c3 (Bind Abbr) w) c2)).(eq_ind C
  89 (CHead c3 (Bind Abbr) w) (\lambda (c: C).((csubc g e c3) \to ((sc3 g (asucc g
  90 a) e u) \to ((sc3 g a c3 w) \to (ex2 C (\lambda (e2: C).(clear c e2))
  91 (\lambda (e2: C).(csubc g (CHead e (Bind Abst) u) e2))))))) (\lambda (H12:
  92 (csubc g e c3)).(\lambda (H13: (sc3 g (asucc g a) e u)).(\lambda (H14: (sc3 g
  93 a c3 w)).(ex_intro2 C (\lambda (e2: C).(clear (CHead c3 (Bind Abbr) w) e2))
  94 (\lambda (e2: C).(csubc g (CHead e (Bind Abst) u) e2)) (CHead c3 (Bind Abbr)
  95 w) (clear_bind Abbr c3 w) (csubc_abst g e c3 H12 u a H13 w H14))))) c2 H11))
  96 v (sym_eq T v u H10))) b H9)) c0 (sym_eq C c0 e H8))) H7)) H6)) H5 H1 H2
  97 H3)))]) in (H1 (refl_equal C (CHead e (Bind b) u)) (refl_equal C c2))))))))
  98 (\lambda (e: C).(\lambda (c: C).(\lambda (_: (clear e c)).(\lambda (H1:
  99 ((\forall (c2: C).((csubc g e c2) \to (ex2 C (\lambda (e2: C).(clear c2 e2))
 100 (\lambda (e2: C).(csubc g c e2))))))).(\lambda (f: F).(\lambda (u:
 101 T).(\lambda (c2: C).(\lambda (H2: (csubc g (CHead e (Flat f) u) c2)).(let H3
 102 \def (match H2 in csubc return (\lambda (c0: C).(\lambda (c3: C).(\lambda (_:
 103 (csubc ? c0 c3)).((eq C c0 (CHead e (Flat f) u)) \to ((eq C c3 c2) \to (ex2 C
 104 (\lambda (e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g c e2)))))))) with
 105 [(csubc_sort n) \Rightarrow (\lambda (H3: (eq C (CSort n) (CHead e (Flat f)
 106 u))).(\lambda (H4: (eq C (CSort n) c2)).((let H5 \def (eq_ind C (CSort n)
 107 (\lambda (e0: C).(match e0 in C return (\lambda (_: C).Prop) with [(CSort _)
 108 \Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e (Flat f) u)
 109 H3) in (False_ind ((eq C (CSort n) c2) \to (ex2 C (\lambda (e2: C).(clear c2
 110 e2)) (\lambda (e2: C).(csubc g c e2)))) H5)) H4))) | (csubc_head c0 c3 H3 k
 111 v) \Rightarrow (\lambda (H4: (eq C (CHead c0 k v) (CHead e (Flat f)
 112 u))).(\lambda (H5: (eq C (CHead c3 k v) c2)).((let H6 \def (f_equal C T
 113 (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with [(CSort _)
 114 \Rightarrow v | (CHead _ _ t) \Rightarrow t])) (CHead c0 k v) (CHead e (Flat
 115 f) u) H4) in ((let H7 \def (f_equal C K (\lambda (e0: C).(match e0 in C
 116 return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k0 _)
 117 \Rightarrow k0])) (CHead c0 k v) (CHead e (Flat f) u) H4) in ((let H8 \def
 118 (f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
 119 [(CSort _) \Rightarrow c0 | (CHead c4 _ _) \Rightarrow c4])) (CHead c0 k v)
 120 (CHead e (Flat f) u) H4) in (eq_ind C e (\lambda (c4: C).((eq K k (Flat f))
 121 \to ((eq T v u) \to ((eq C (CHead c3 k v) c2) \to ((csubc g c4 c3) \to (ex2 C
 122 (\lambda (e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g c e2))))))))
 123 (\lambda (H9: (eq K k (Flat f))).(eq_ind K (Flat f) (\lambda (k0: K).((eq T v
 124 u) \to ((eq C (CHead c3 k0 v) c2) \to ((csubc g e c3) \to (ex2 C (\lambda
 125 (e2: C).(clear c2 e2)) (\lambda (e2: C).(csubc g c e2))))))) (\lambda (H10:
 126 (eq T v u)).(eq_ind T u (\lambda (t: T).((eq C (CHead c3 (Flat f) t) c2) \to
 127 ((csubc g e c3) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda (e2:
 128 C).(csubc g c e2)))))) (\lambda (H11: (eq C (CHead c3 (Flat f) u)
 129 c2)).(eq_ind C (CHead c3 (Flat f) u) (\lambda (c4: C).((csubc g e c3) \to
 130 (ex2 C (\lambda (e2: C).(clear c4 e2)) (\lambda (e2: C).(csubc g c e2)))))
 131 (\lambda (H12: (csubc g e c3)).(let H_x \def (H1 c3 H12) in (let H13 \def H_x
 132 in (ex2_ind C (\lambda (e2: C).(clear c3 e2)) (\lambda (e2: C).(csubc g c
 133 e2)) (ex2 C (\lambda (e2: C).(clear (CHead c3 (Flat f) u) e2)) (\lambda (e2:
 134 C).(csubc g c e2))) (\lambda (x: C).(\lambda (H14: (clear c3 x)).(\lambda
 135 (H15: (csubc g c x)).(ex_intro2 C (\lambda (e2: C).(clear (CHead c3 (Flat f)
 136 u) e2)) (\lambda (e2: C).(csubc g c e2)) x (clear_flat c3 x H14 f u) H15))))
 137 H13)))) c2 H11)) v (sym_eq T v u H10))) k (sym_eq K k (Flat f) H9))) c0
 138 (sym_eq C c0 e H8))) H7)) H6)) H5 H3))) | (csubc_abst c0 c3 H3 v a H4 w H5)
 139 \Rightarrow (\lambda (H6: (eq C (CHead c0 (Bind Abst) v) (CHead e (Flat f)
 140 u))).(\lambda (H7: (eq C (CHead c3 (Bind Abbr) w) c2)).((let H8 \def (eq_ind
 141 C (CHead c0 (Bind Abst) v) (\lambda (e0: C).(match e0 in C return (\lambda
 142 (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow
 143 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True |
 144 (Flat _) \Rightarrow False])])) I (CHead e (Flat f) u) H6) in (False_ind ((eq
 145 C (CHead c3 (Bind Abbr) w) c2) \to ((csubc g c0 c3) \to ((sc3 g (asucc g a)
 146 c0 v) \to ((sc3 g a c3 w) \to (ex2 C (\lambda (e2: C).(clear c2 e2)) (\lambda
 147 (e2: C).(csubc g c e2))))))) H8)) H7 H3 H4 H5)))]) in (H3 (refl_equal C
 148 (CHead e (Flat f) u)) (refl_equal C c2))))))))))) c1 e1 H)))).
 149