helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ceqc/props.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/ceqc/props".
  18
  19 include "ceqc/defs.ma".
  20
  21 include "sc3/props.ma".
  22
  23 theorem csubc_refl:
  24  \forall (g: G).(\forall (c: C).(csubc g c c))
  25 \def
  26  \lambda (g: G).(\lambda (c: C).(C_ind (\lambda (c0: C).(csubc g c0 c0))
  27 (\lambda (n: nat).(csubc_sort g n)) (\lambda (c0: C).(\lambda (H: (csubc g c0
  28 c0)).(\lambda (k: K).(\lambda (t: T).(csubc_head g c0 c0 H k t))))) c)).
  29
  30 theorem ceqc_sym:
  31  \forall (g: G).(\forall (c1: C).(\forall (c2: C).((ceqc g c1 c2) \to (ceqc g
  32 c2 c1))))
  33 \def
  34  \lambda (g: G).(\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (ceqc g c1
  35 c2)).(let H0 \def H in (or_ind (csubc g c1 c2) (csubc g c2 c1) (ceqc g c2 c1)
  36 (\lambda (H1: (csubc g c1 c2)).(or_intror (csubc g c2 c1) (csubc g c1 c2)
  37 H1)) (\lambda (H1: (csubc g c2 c1)).(or_introl (csubc g c2 c1) (csubc g c1
  38 c2) H1)) H0))))).
  39
  40 theorem drop_csubc_trans:
  41  \forall (g: G).(\forall (c2: C).(\forall (e2: C).(\forall (d: nat).(\forall
  42 (h: nat).((drop h d c2 e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C
  43 (\lambda (c1: C).(drop h d c1 e1)) (\lambda (c1: C).(csubc g c2 c1))))))))))
  44 \def
  45  \lambda (g: G).(\lambda (c2: C).(C_ind (\lambda (c: C).(\forall (e2:
  46 C).(\forall (d: nat).(\forall (h: nat).((drop h d c e2) \to (\forall (e1:
  47 C).((csubc g e2 e1) \to (ex2 C (\lambda (c1: C).(drop h d c1 e1)) (\lambda
  48 (c1: C).(csubc g c c1)))))))))) (\lambda (n: nat).(\lambda (e2: C).(\lambda
  49 (d: nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n) e2)).(\lambda
  50 (e1: C).(\lambda (H0: (csubc g e2 e1)).(and3_ind (eq C e2 (CSort n)) (eq nat
  51 h O) (eq nat d O) (ex2 C (\lambda (c1: C).(drop h d c1 e1)) (\lambda (c1:
  52 C).(csubc g (CSort n) c1))) (\lambda (H1: (eq C e2 (CSort n))).(\lambda (H2:
  53 (eq nat h O)).(\lambda (H3: (eq nat d O)).(eq_ind_r nat O (\lambda (n0:
  54 nat).(ex2 C (\lambda (c1: C).(drop n0 d c1 e1)) (\lambda (c1: C).(csubc g
  55 (CSort n) c1)))) (eq_ind_r nat O (\lambda (n0: nat).(ex2 C (\lambda (c1:
  56 C).(drop O n0 c1 e1)) (\lambda (c1: C).(csubc g (CSort n) c1)))) (let H4 \def
  57 (eq_ind C e2 (\lambda (c: C).(csubc g c e1)) H0 (CSort n) H1) in (ex_intro2 C
  58 (\lambda (c1: C).(drop O O c1 e1)) (\lambda (c1: C).(csubc g (CSort n) c1))
  59 e1 (drop_refl e1) H4)) d H3) h H2)))) (drop_gen_sort n h d e2 H)))))))))
  60 (\lambda (c: C).(\lambda (H: ((\forall (e2: C).(\forall (d: nat).(\forall (h:
  61 nat).((drop h d c e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C
  62 (\lambda (c1: C).(drop h d c1 e1)) (\lambda (c1: C).(csubc g c
  63 c1))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e2: C).(\lambda (d:
  64 nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n (CHead c k t)
  65 e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C (\lambda (c1: C).(drop h
  66 n c1 e1)) (\lambda (c1: C).(csubc g (CHead c k t) c1)))))))) (\lambda (h:
  67 nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c k t) e2) \to (\forall
  68 (e1: C).((csubc g e2 e1) \to (ex2 C (\lambda (c1: C).(drop n O c1 e1))
  69 (\lambda (c1: C).(csubc g (CHead c k t) c1))))))) (\lambda (H0: (drop O O
  70 (CHead c k t) e2)).(\lambda (e1: C).(\lambda (H1: (csubc g e2 e1)).(let H2
  71 \def (eq_ind_r C e2 (\lambda (c0: C).(csubc g c0 e1)) H1 (CHead c k t)
  72 (drop_gen_refl (CHead c k t) e2 H0)) in (ex_intro2 C (\lambda (c1: C).(drop O
  73 O c1 e1)) (\lambda (c1: C).(csubc g (CHead c k t) c1)) e1 (drop_refl e1)
  74 H2))))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c k t) e2) \to
  75 (\forall (e1: C).((csubc g e2 e1) \to (ex2 C (\lambda (c1: C).(drop n O c1
  76 e1)) (\lambda (c1: C).(csubc g (CHead c k t) c1)))))))).(\lambda (H1: (drop
  77 (S n) O (CHead c k t) e2)).(\lambda (e1: C).(\lambda (H2: (csubc g e2
  78 e1)).(let H_x \def (H e2 O (r k n) (drop_gen_drop k c e2 t n H1) e1 H2) in
  79 (let H3 \def H_x in (ex2_ind C (\lambda (c1: C).(drop (r k n) O c1 e1))
  80 (\lambda (c1: C).(csubc g c c1)) (ex2 C (\lambda (c1: C).(drop (S n) O c1
  81 e1)) (\lambda (c1: C).(csubc g (CHead c k t) c1))) (\lambda (x: C).(\lambda
  82 (H4: (drop (r k n) O x e1)).(\lambda (H5: (csubc g c x)).(ex_intro2 C
  83 (\lambda (c1: C).(drop (S n) O c1 e1)) (\lambda (c1: C).(csubc g (CHead c k
  84 t) c1)) (CHead x k t) (drop_drop k n x e1 H4 t) (csubc_head g c x H5 k t)))))
  85 H3)))))))) h)) (\lambda (n: nat).(\lambda (H0: ((\forall (h: nat).((drop h n
  86 (CHead c k t) e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C (\lambda
  87 (c1: C).(drop h n c1 e1)) (\lambda (c1: C).(csubc g (CHead c k t)
  88 c1))))))))).(\lambda (h: nat).(\lambda (H1: (drop h (S n) (CHead c k t)
  89 e2)).(\lambda (e1: C).(\lambda (H2: (csubc g e2 e1)).(ex3_2_ind C T (\lambda
  90 (e: C).(\lambda (v: T).(eq C e2 (CHead e k v)))) (\lambda (_: C).(\lambda (v:
  91 T).(eq T t (lift h (r k n) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k
  92 n) c e))) (ex2 C (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1:
  93 C).(csubc g (CHead c k t) c1))) (\lambda (x0: C).(\lambda (x1: T).(\lambda
  94 (H3: (eq C e2 (CHead x0 k x1))).(\lambda (H4: (eq T t (lift h (r k n)
  95 x1))).(\lambda (H5: (drop h (r k n) c x0)).(let H6 \def (eq_ind C e2 (\lambda
  96 (c0: C).(csubc g c0 e1)) H2 (CHead x0 k x1) H3) in (let H7 \def (eq_ind C e2
  97 (\lambda (c0: C).(\forall (h0: nat).((drop h0 n (CHead c k t) c0) \to
  98 (\forall (e3: C).((csubc g c0 e3) \to (ex2 C (\lambda (c1: C).(drop h0 n c1
  99 e3)) (\lambda (c1: C).(csubc g (CHead c k t) c1)))))))) H0 (CHead x0 k x1)
 100 H3) in (let H8 \def (eq_ind T t (\lambda (t0: T).(\forall (h0: nat).((drop h0
 101 n (CHead c k t0) (CHead x0 k x1)) \to (\forall (e3: C).((csubc g (CHead x0 k
 102 x1) e3) \to (ex2 C (\lambda (c1: C).(drop h0 n c1 e3)) (\lambda (c1:
 103 C).(csubc g (CHead c k t0) c1)))))))) H7 (lift h (r k n) x1) H4) in (eq_ind_r
 104 T (lift h (r k n) x1) (\lambda (t0: T).(ex2 C (\lambda (c1: C).(drop h (S n)
 105 c1 e1)) (\lambda (c1: C).(csubc g (CHead c k t0) c1)))) (let H9 \def (match
 106 H6 in csubc return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csubc ? c0
 107 c1)).((eq C c0 (CHead x0 k x1)) \to ((eq C c1 e1) \to (ex2 C (\lambda (c3:
 108 C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n)
 109 x1)) c3)))))))) with [(csubc_sort n0) \Rightarrow (\lambda (H9: (eq C (CSort
 110 n0) (CHead x0 k x1))).(\lambda (H10: (eq C (CSort n0) e1)).((let H11 \def
 111 (eq_ind C (CSort n0) (\lambda (e: C).(match e in C return (\lambda (_:
 112 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
 113 False])) I (CHead x0 k x1) H9) in (False_ind ((eq C (CSort n0) e1) \to (ex2 C
 114 (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1: C).(csubc g (CHead c k
 115 (lift h (r k n) x1)) c1)))) H11)) H10))) | (csubc_head c1 c0 H9 k0 v)
 116 \Rightarrow (\lambda (H10: (eq C (CHead c1 k0 v) (CHead x0 k x1))).(\lambda
 117 (H11: (eq C (CHead c0 k0 v) e1)).((let H12 \def (f_equal C T (\lambda (e:
 118 C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v |
 119 (CHead _ _ t0) \Rightarrow t0])) (CHead c1 k0 v) (CHead x0 k x1) H10) in
 120 ((let H13 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_:
 121 C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1]))
 122 (CHead c1 k0 v) (CHead x0 k x1) H10) in ((let H14 \def (f_equal C C (\lambda
 123 (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1
 124 | (CHead c3 _ _) \Rightarrow c3])) (CHead c1 k0 v) (CHead x0 k x1) H10) in
 125 (eq_ind C x0 (\lambda (c3: C).((eq K k0 k) \to ((eq T v x1) \to ((eq C (CHead
 126 c0 k0 v) e1) \to ((csubc g c3 c0) \to (ex2 C (\lambda (c4: C).(drop h (S n)
 127 c4 e1)) (\lambda (c4: C).(csubc g (CHead c k (lift h (r k n) x1)) c4))))))))
 128 (\lambda (H15: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T v x1) \to
 129 ((eq C (CHead c0 k1 v) e1) \to ((csubc g x0 c0) \to (ex2 C (\lambda (c3:
 130 C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n)
 131 x1)) c3))))))) (\lambda (H16: (eq T v x1)).(eq_ind T x1 (\lambda (t0: T).((eq
 132 C (CHead c0 k t0) e1) \to ((csubc g x0 c0) \to (ex2 C (\lambda (c3: C).(drop
 133 h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n) x1))
 134 c3)))))) (\lambda (H17: (eq C (CHead c0 k x1) e1)).(eq_ind C (CHead c0 k x1)
 135 (\lambda (c3: C).((csubc g x0 c0) \to (ex2 C (\lambda (c4: C).(drop h (S n)
 136 c4 c3)) (\lambda (c4: C).(csubc g (CHead c k (lift h (r k n) x1)) c4)))))
 137 (\lambda (H18: (csubc g x0 c0)).(let H_x \def (H x0 (r k n) h H5 c0 H18) in
 138 (let H19 \def H_x in (ex2_ind C (\lambda (c3: C).(drop h (r k n) c3 c0))
 139 (\lambda (c3: C).(csubc g c c3)) (ex2 C (\lambda (c3: C).(drop h (S n) c3
 140 (CHead c0 k x1))) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n) x1))
 141 c3))) (\lambda (x: C).(\lambda (H20: (drop h (r k n) x c0)).(\lambda (H21:
 142 (csubc g c x)).(ex_intro2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c0 k
 143 x1))) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n) x1)) c3)) (CHead x
 144 k (lift h (r k n) x1)) (drop_skip k h n x c0 H20 x1) (csubc_head g c x H21 k
 145 (lift h (r k n) x1)))))) H19)))) e1 H17)) v (sym_eq T v x1 H16))) k0 (sym_eq
 146 K k0 k H15))) c1 (sym_eq C c1 x0 H14))) H13)) H12)) H11 H9))) | (csubc_abst
 147 c1 c0 H9 v a H10 w H11) \Rightarrow (\lambda (H12: (eq C (CHead c1 (Bind
 148 Abst) v) (CHead x0 k x1))).(\lambda (H13: (eq C (CHead c0 (Bind Abbr) w)
 149 e1)).((let H14 \def (f_equal C T (\lambda (e: C).(match e in C return
 150 (\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t0) \Rightarrow
 151 t0])) (CHead c1 (Bind Abst) v) (CHead x0 k x1) H12) in ((let H15 \def
 152 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
 153 [(CSort _) \Rightarrow (Bind Abst) | (CHead _ k0 _) \Rightarrow k0])) (CHead
 154 c1 (Bind Abst) v) (CHead x0 k x1) H12) in ((let H16 \def (f_equal C C
 155 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
 156 \Rightarrow c1 | (CHead c3 _ _) \Rightarrow c3])) (CHead c1 (Bind Abst) v)
 157 (CHead x0 k x1) H12) in (eq_ind C x0 (\lambda (c3: C).((eq K (Bind Abst) k)
 158 \to ((eq T v x1) \to ((eq C (CHead c0 (Bind Abbr) w) e1) \to ((csubc g c3 c0)
 159 \to ((sc3 g (asucc g a) c3 v) \to ((sc3 g a c0 w) \to (ex2 C (\lambda (c4:
 160 C).(drop h (S n) c4 e1)) (\lambda (c4: C).(csubc g (CHead c k (lift h (r k n)
 161 x1)) c4)))))))))) (\lambda (H17: (eq K (Bind Abst) k)).(eq_ind K (Bind Abst)
 162 (\lambda (k0: K).((eq T v x1) \to ((eq C (CHead c0 (Bind Abbr) w) e1) \to
 163 ((csubc g x0 c0) \to ((sc3 g (asucc g a) x0 v) \to ((sc3 g a c0 w) \to (ex2 C
 164 (\lambda (c3: C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k0
 165 (lift h (r k0 n) x1)) c3))))))))) (\lambda (H18: (eq T v x1)).(eq_ind T x1
 166 (\lambda (t0: T).((eq C (CHead c0 (Bind Abbr) w) e1) \to ((csubc g x0 c0) \to
 167 ((sc3 g (asucc g a) x0 t0) \to ((sc3 g a c0 w) \to (ex2 C (\lambda (c3:
 168 C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c (Bind Abst) (lift
 169 h (r (Bind Abst) n) x1)) c3)))))))) (\lambda (H19: (eq C (CHead c0 (Bind
 170 Abbr) w) e1)).(eq_ind C (CHead c0 (Bind Abbr) w) (\lambda (c3: C).((csubc g
 171 x0 c0) \to ((sc3 g (asucc g a) x0 x1) \to ((sc3 g a c0 w) \to (ex2 C (\lambda
 172 (c4: C).(drop h (S n) c4 c3)) (\lambda (c4: C).(csubc g (CHead c (Bind Abst)
 173 (lift h (r (Bind Abst) n) x1)) c4))))))) (\lambda (H20: (csubc g x0
 174 c0)).(\lambda (H21: (sc3 g (asucc g a) x0 x1)).(\lambda (H22: (sc3 g a c0
 175 w)).(let H23 \def (eq_ind_r K k (\lambda (k0: K).(\forall (h0: nat).((drop h0
 176 n (CHead c k0 (lift h (r k0 n) x1)) (CHead x0 k0 x1)) \to (\forall (e3:
 177 C).((csubc g (CHead x0 k0 x1) e3) \to (ex2 C (\lambda (c3: C).(drop h0 n c3
 178 e3)) (\lambda (c3: C).(csubc g (CHead c k0 (lift h (r k0 n) x1)) c3))))))))
 179 H8 (Bind Abst) H17) in (let H24 \def (eq_ind_r K k (\lambda (k0: K).(drop h
 180 (r k0 n) c x0)) H5 (Bind Abst) H17) in (let H_x \def (H x0 (r (Bind Abst) n)
 181 h H24 c0 H20) in (let H25 \def H_x in (ex2_ind C (\lambda (c3: C).(drop h (r
 182 (Bind Abst) n) c3 c0)) (\lambda (c3: C).(csubc g c c3)) (ex2 C (\lambda (c3:
 183 C).(drop h (S n) c3 (CHead c0 (Bind Abbr) w))) (\lambda (c3: C).(csubc g
 184 (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) c3))) (\lambda (x:
 185 C).(\lambda (H26: (drop h (r (Bind Abst) n) x c0)).(\lambda (H27: (csubc g c
 186 x)).(ex_intro2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c0 (Bind Abbr) w)))
 187 (\lambda (c3: C).(csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1))
 188 c3)) (CHead x (Bind Abbr) (lift h n w)) (drop_skip_bind h n x c0 H26 Abbr w)
 189 (csubc_abst g c x H27 (lift h (r (Bind Abst) n) x1) a (sc3_lift g (asucc g a)
 190 x0 x1 H21 c h (r (Bind Abst) n) H24) (lift h n w) (sc3_lift g a c0 w H22 x h
 191 n H26)))))) H25)))))))) e1 H19)) v (sym_eq T v x1 H18))) k H17)) c1 (sym_eq C
 192 c1 x0 H16))) H15)) H14)) H13 H9 H10 H11)))]) in (H9 (refl_equal C (CHead x0 k
 193 x1)) (refl_equal C e1))) t H4))))))))) (drop_gen_skip_l c e2 t h n k
 194 H1)))))))) d))))))) c2)).
 195
 196 theorem csubc_drop_conf_rev:
 197  \forall (g: G).(\forall (c2: C).(\forall (e2: C).(\forall (d: nat).(\forall
 198 (h: nat).((drop h d c2 e2) \to (\forall (e1: C).((csubc g e1 e2) \to (ex2 C
 199 (\lambda (c1: C).(drop h d c1 e1)) (\lambda (c1: C).(csubc g c1 c2))))))))))
 200 \def
 201  \lambda (g: G).(\lambda (c2: C).(C_ind (\lambda (c: C).(\forall (e2:
 202 C).(\forall (d: nat).(\forall (h: nat).((drop h d c e2) \to (\forall (e1:
 203 C).((csubc g e1 e2) \to (ex2 C (\lambda (c1: C).(drop h d c1 e1)) (\lambda
 204 (c1: C).(csubc g c1 c)))))))))) (\lambda (n: nat).(\lambda (e2: C).(\lambda
 205 (d: nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n) e2)).(\lambda
 206 (e1: C).(\lambda (H0: (csubc g e1 e2)).(and3_ind (eq C e2 (CSort n)) (eq nat
 207 h O) (eq nat d O) (ex2 C (\lambda (c1: C).(drop h d c1 e1)) (\lambda (c1:
 208 C).(csubc g c1 (CSort n)))) (\lambda (H1: (eq C e2 (CSort n))).(\lambda (H2:
 209 (eq nat h O)).(\lambda (H3: (eq nat d O)).(eq_ind_r nat O (\lambda (n0:
 210 nat).(ex2 C (\lambda (c1: C).(drop n0 d c1 e1)) (\lambda (c1: C).(csubc g c1
 211 (CSort n))))) (eq_ind_r nat O (\lambda (n0: nat).(ex2 C (\lambda (c1:
 212 C).(drop O n0 c1 e1)) (\lambda (c1: C).(csubc g c1 (CSort n))))) (let H4 \def
 213 (eq_ind C e2 (\lambda (c: C).(csubc g e1 c)) H0 (CSort n) H1) in (ex_intro2 C
 214 (\lambda (c1: C).(drop O O c1 e1)) (\lambda (c1: C).(csubc g c1 (CSort n)))
 215 e1 (drop_refl e1) H4)) d H3) h H2)))) (drop_gen_sort n h d e2 H)))))))))
 216 (\lambda (c: C).(\lambda (H: ((\forall (e2: C).(\forall (d: nat).(\forall (h:
 217 nat).((drop h d c e2) \to (\forall (e1: C).((csubc g e1 e2) \to (ex2 C
 218 (\lambda (c1: C).(drop h d c1 e1)) (\lambda (c1: C).(csubc g c1
 219 c))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e2: C).(\lambda (d:
 220 nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n (CHead c k t)
 221 e2) \to (\forall (e1: C).((csubc g e1 e2) \to (ex2 C (\lambda (c1: C).(drop h
 222 n c1 e1)) (\lambda (c1: C).(csubc g c1 (CHead c k t))))))))) (\lambda (h:
 223 nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c k t) e2) \to (\forall
 224 (e1: C).((csubc g e1 e2) \to (ex2 C (\lambda (c1: C).(drop n O c1 e1))
 225 (\lambda (c1: C).(csubc g c1 (CHead c k t)))))))) (\lambda (H0: (drop O O
 226 (CHead c k t) e2)).(\lambda (e1: C).(\lambda (H1: (csubc g e1 e2)).(let H2
 227 \def (eq_ind_r C e2 (\lambda (c0: C).(csubc g e1 c0)) H1 (CHead c k t)
 228 (drop_gen_refl (CHead c k t) e2 H0)) in (ex_intro2 C (\lambda (c1: C).(drop O
 229 O c1 e1)) (\lambda (c1: C).(csubc g c1 (CHead c k t))) e1 (drop_refl e1)
 230 H2))))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c k t) e2) \to
 231 (\forall (e1: C).((csubc g e1 e2) \to (ex2 C (\lambda (c1: C).(drop n O c1
 232 e1)) (\lambda (c1: C).(csubc g c1 (CHead c k t))))))))).(\lambda (H1: (drop
 233 (S n) O (CHead c k t) e2)).(\lambda (e1: C).(\lambda (H2: (csubc g e1
 234 e2)).(let H_x \def (H e2 O (r k n) (drop_gen_drop k c e2 t n H1) e1 H2) in
 235 (let H3 \def H_x in (ex2_ind C (\lambda (c1: C).(drop (r k n) O c1 e1))
 236 (\lambda (c1: C).(csubc g c1 c)) (ex2 C (\lambda (c1: C).(drop (S n) O c1
 237 e1)) (\lambda (c1: C).(csubc g c1 (CHead c k t)))) (\lambda (x: C).(\lambda
 238 (H4: (drop (r k n) O x e1)).(\lambda (H5: (csubc g x c)).(ex_intro2 C
 239 (\lambda (c1: C).(drop (S n) O c1 e1)) (\lambda (c1: C).(csubc g c1 (CHead c
 240 k t))) (CHead x k t) (drop_drop k n x e1 H4 t) (csubc_head g x c H5 k t)))))
 241 H3)))))))) h)) (\lambda (n: nat).(\lambda (H0: ((\forall (h: nat).((drop h n
 242 (CHead c k t) e2) \to (\forall (e1: C).((csubc g e1 e2) \to (ex2 C (\lambda
 243 (c1: C).(drop h n c1 e1)) (\lambda (c1: C).(csubc g c1 (CHead c k
 244 t)))))))))).(\lambda (h: nat).(\lambda (H1: (drop h (S n) (CHead c k t)
 245 e2)).(\lambda (e1: C).(\lambda (H2: (csubc g e1 e2)).(ex3_2_ind C T (\lambda
 246 (e: C).(\lambda (v: T).(eq C e2 (CHead e k v)))) (\lambda (_: C).(\lambda (v:
 247 T).(eq T t (lift h (r k n) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k
 248 n) c e))) (ex2 C (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1:
 249 C).(csubc g c1 (CHead c k t)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda
 250 (H3: (eq C e2 (CHead x0 k x1))).(\lambda (H4: (eq T t (lift h (r k n)
 251 x1))).(\lambda (H5: (drop h (r k n) c x0)).(let H6 \def (eq_ind C e2 (\lambda
 252 (c0: C).(csubc g e1 c0)) H2 (CHead x0 k x1) H3) in (let H7 \def (eq_ind C e2
 253 (\lambda (c0: C).(\forall (h0: nat).((drop h0 n (CHead c k t) c0) \to
 254 (\forall (e3: C).((csubc g e3 c0) \to (ex2 C (\lambda (c1: C).(drop h0 n c1
 255 e3)) (\lambda (c1: C).(csubc g c1 (CHead c k t))))))))) H0 (CHead x0 k x1)
 256 H3) in (let H8 \def (eq_ind T t (\lambda (t0: T).(\forall (h0: nat).((drop h0
 257 n (CHead c k t0) (CHead x0 k x1)) \to (\forall (e3: C).((csubc g e3 (CHead x0
 258 k x1)) \to (ex2 C (\lambda (c1: C).(drop h0 n c1 e3)) (\lambda (c1: C).(csubc
 259 g c1 (CHead c k t0))))))))) H7 (lift h (r k n) x1) H4) in (eq_ind_r T (lift h
 260 (r k n) x1) (\lambda (t0: T).(ex2 C (\lambda (c1: C).(drop h (S n) c1 e1))
 261 (\lambda (c1: C).(csubc g c1 (CHead c k t0))))) (let H9 \def (match H6 in
 262 csubc return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csubc ? c0
 263 c1)).((eq C c0 e1) \to ((eq C c1 (CHead x0 k x1)) \to (ex2 C (\lambda (c3:
 264 C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g c3 (CHead c k (lift h (r k
 265 n) x1)))))))))) with [(csubc_sort n0) \Rightarrow (\lambda (H9: (eq C (CSort
 266 n0) e1)).(\lambda (H10: (eq C (CSort n0) (CHead x0 k x1))).(eq_ind C (CSort
 267 n0) (\lambda (c0: C).((eq C (CSort n0) (CHead x0 k x1)) \to (ex2 C (\lambda
 268 (c1: C).(drop h (S n) c1 c0)) (\lambda (c1: C).(csubc g c1 (CHead c k (lift h
 269 (r k n) x1))))))) (\lambda (H11: (eq C (CSort n0) (CHead x0 k x1))).(let H12
 270 \def (eq_ind C (CSort n0) (\lambda (e: C).(match e in C return (\lambda (_:
 271 C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
 272 False])) I (CHead x0 k x1) H11) in (False_ind (ex2 C (\lambda (c1: C).(drop h
 273 (S n) c1 (CSort n0))) (\lambda (c1: C).(csubc g c1 (CHead c k (lift h (r k n)
 274 x1))))) H12))) e1 H9 H10))) | (csubc_head c1 c0 H9 k0 v) \Rightarrow (\lambda
 275 (H10: (eq C (CHead c1 k0 v) e1)).(\lambda (H11: (eq C (CHead c0 k0 v) (CHead
 276 x0 k x1))).(eq_ind C (CHead c1 k0 v) (\lambda (c3: C).((eq C (CHead c0 k0 v)
 277 (CHead x0 k x1)) \to ((csubc g c1 c0) \to (ex2 C (\lambda (c4: C).(drop h (S
 278 n) c4 c3)) (\lambda (c4: C).(csubc g c4 (CHead c k (lift h (r k n) x1))))))))
 279 (\lambda (H12: (eq C (CHead c0 k0 v) (CHead x0 k x1))).(let H13 \def (f_equal
 280 C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
 281 \Rightarrow v | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 k0 v) (CHead x0 k
 282 x1) H12) in ((let H14 \def (f_equal C K (\lambda (e: C).(match e in C return
 283 (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1 _)
 284 \Rightarrow k1])) (CHead c0 k0 v) (CHead x0 k x1) H12) in ((let H15 \def
 285 (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
 286 [(CSort _) \Rightarrow c0 | (CHead c3 _ _) \Rightarrow c3])) (CHead c0 k0 v)
 287 (CHead x0 k x1) H12) in (eq_ind C x0 (\lambda (c3: C).((eq K k0 k) \to ((eq T
 288 v x1) \to ((csubc g c1 c3) \to (ex2 C (\lambda (c4: C).(drop h (S n) c4
 289 (CHead c1 k0 v))) (\lambda (c4: C).(csubc g c4 (CHead c k (lift h (r k n)
 290 x1))))))))) (\lambda (H16: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T v
 291 x1) \to ((csubc g c1 x0) \to (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead
 292 c1 k1 v))) (\lambda (c3: C).(csubc g c3 (CHead c k (lift h (r k n) x1))))))))
 293 (\lambda (H17: (eq T v x1)).(eq_ind T x1 (\lambda (t0: T).((csubc g c1 x0)
 294 \to (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1 k t0))) (\lambda (c3:
 295 C).(csubc g c3 (CHead c k (lift h (r k n) x1))))))) (\lambda (H18: (csubc g
 296 c1 x0)).(let H19 \def (eq_ind T v (\lambda (t0: T).(eq C (CHead c1 k0 t0)
 297 e1)) H10 x1 H17) in (let H20 \def (eq_ind K k0 (\lambda (k1: K).(eq C (CHead
 298 c1 k1 x1) e1)) H19 k H16) in (let H_x \def (H x0 (r k n) h H5 c1 H18) in (let
 299 H21 \def H_x in (ex2_ind C (\lambda (c3: C).(drop h (r k n) c3 c1)) (\lambda
 300 (c3: C).(csubc g c3 c)) (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1 k
 301 x1))) (\lambda (c3: C).(csubc g c3 (CHead c k (lift h (r k n) x1)))))
 302 (\lambda (x: C).(\lambda (H22: (drop h (r k n) x c1)).(\lambda (H23: (csubc g
 303 x c)).(ex_intro2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1 k x1)))
 304 (\lambda (c3: C).(csubc g c3 (CHead c k (lift h (r k n) x1)))) (CHead x k
 305 (lift h (r k n) x1)) (drop_skip k h n x c1 H22 x1) (csubc_head g x c H23 k
 306 (lift h (r k n) x1)))))) H21)))))) v (sym_eq T v x1 H17))) k0 (sym_eq K k0 k
 307 H16))) c0 (sym_eq C c0 x0 H15))) H14)) H13))) e1 H10 H11 H9))) | (csubc_abst
 308 c1 c0 H9 v a H10 w H11) \Rightarrow (\lambda (H12: (eq C (CHead c1 (Bind
 309 Abst) v) e1)).(\lambda (H13: (eq C (CHead c0 (Bind Abbr) w) (CHead x0 k
 310 x1))).(eq_ind C (CHead c1 (Bind Abst) v) (\lambda (c3: C).((eq C (CHead c0
 311 (Bind Abbr) w) (CHead x0 k x1)) \to ((csubc g c1 c0) \to ((sc3 g (asucc g a)
 312 c1 v) \to ((sc3 g a c0 w) \to (ex2 C (\lambda (c4: C).(drop h (S n) c4 c3))
 313 (\lambda (c4: C).(csubc g c4 (CHead c k (lift h (r k n) x1)))))))))) (\lambda
 314 (H14: (eq C (CHead c0 (Bind Abbr) w) (CHead x0 k x1))).(let H15 \def (f_equal
 315 C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
 316 \Rightarrow w | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 (Bind Abbr) w)
 317 (CHead x0 k x1) H14) in ((let H16 \def (f_equal C K (\lambda (e: C).(match e
 318 in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow (Bind Abbr) |
 319 (CHead _ k0 _) \Rightarrow k0])) (CHead c0 (Bind Abbr) w) (CHead x0 k x1)
 320 H14) in ((let H17 \def (f_equal C C (\lambda (e: C).(match e in C return
 321 (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c3 _ _)
 322 \Rightarrow c3])) (CHead c0 (Bind Abbr) w) (CHead x0 k x1) H14) in (eq_ind C
 323 x0 (\lambda (c3: C).((eq K (Bind Abbr) k) \to ((eq T w x1) \to ((csubc g c1
 324 c3) \to ((sc3 g (asucc g a) c1 v) \to ((sc3 g a c3 w) \to (ex2 C (\lambda
 325 (c4: C).(drop h (S n) c4 (CHead c1 (Bind Abst) v))) (\lambda (c4: C).(csubc g
 326 c4 (CHead c k (lift h (r k n) x1))))))))))) (\lambda (H18: (eq K (Bind Abbr)
 327 k)).(eq_ind K (Bind Abbr) (\lambda (k0: K).((eq T w x1) \to ((csubc g c1 x0)
 328 \to ((sc3 g (asucc g a) c1 v) \to ((sc3 g a x0 w) \to (ex2 C (\lambda (c3:
 329 C).(drop h (S n) c3 (CHead c1 (Bind Abst) v))) (\lambda (c3: C).(csubc g c3
 330 (CHead c k0 (lift h (r k0 n) x1)))))))))) (\lambda (H19: (eq T w x1)).(eq_ind
 331 T x1 (\lambda (t0: T).((csubc g c1 x0) \to ((sc3 g (asucc g a) c1 v) \to
 332 ((sc3 g a x0 t0) \to (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1 (Bind
 333 Abst) v))) (\lambda (c3: C).(csubc g c3 (CHead c (Bind Abbr) (lift h (r (Bind
 334 Abbr) n) x1))))))))) (\lambda (H20: (csubc g c1 x0)).(\lambda (H21: (sc3 g
 335 (asucc g a) c1 v)).(\lambda (H22: (sc3 g a x0 x1)).(let H23 \def (eq_ind_r K
 336 k (\lambda (k0: K).(\forall (h0: nat).((drop h0 n (CHead c k0 (lift h (r k0
 337 n) x1)) (CHead x0 k0 x1)) \to (\forall (e3: C).((csubc g e3 (CHead x0 k0 x1))
 338 \to (ex2 C (\lambda (c3: C).(drop h0 n c3 e3)) (\lambda (c3: C).(csubc g c3
 339 (CHead c k0 (lift h (r k0 n) x1)))))))))) H8 (Bind Abbr) H18) in (let H24
 340 \def (eq_ind_r K k (\lambda (k0: K).(drop h (r k0 n) c x0)) H5 (Bind Abbr)
 341 H18) in (let H_x \def (H x0 (r (Bind Abbr) n) h H24 c1 H20) in (let H25 \def
 342 H_x in (ex2_ind C (\lambda (c3: C).(drop h (r (Bind Abbr) n) c3 c1)) (\lambda
 343 (c3: C).(csubc g c3 c)) (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1
 344 (Bind Abst) v))) (\lambda (c3: C).(csubc g c3 (CHead c (Bind Abbr) (lift h (r
 345 (Bind Abbr) n) x1))))) (\lambda (x: C).(\lambda (H26: (drop h (r (Bind Abbr)
 346 n) x c1)).(\lambda (H27: (csubc g x c)).(ex_intro2 C (\lambda (c3: C).(drop h
 347 (S n) c3 (CHead c1 (Bind Abst) v))) (\lambda (c3: C).(csubc g c3 (CHead c
 348 (Bind Abbr) (lift h (r (Bind Abbr) n) x1)))) (CHead x (Bind Abst) (lift h n
 349 v)) (drop_skip_bind h n x c1 H26 Abst v) (csubc_abst g x c H27 (lift h n v) a
 350 (sc3_lift g (asucc g a) c1 v H21 x h n H26) (lift h (r (Bind Abbr) n) x1)
 351 (sc3_lift g a x0 x1 H22 c h (r (Bind Abbr) n) H24)))))) H25)))))))) w (sym_eq
 352 T w x1 H19))) k H18)) c0 (sym_eq C c0 x0 H17))) H16)) H15))) e1 H12 H13 H9
 353 H10 H11)))]) in (H9 (refl_equal C e1) (refl_equal C (CHead x0 k x1)))) t
 354 H4))))))))) (drop_gen_skip_l c e2 t h n k H1)))))))) d))))))) c2)).
 355
 356 theorem drop1_csubc_trans:
 357  \forall (g: G).(\forall (hds: PList).(\forall (c2: C).(\forall (e2:
 358 C).((drop1 hds c2 e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C
 359 (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(csubc g c2 c1)))))))))
 360 \def
 361  \lambda (g: G).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
 362 (c2: C).(\forall (e2: C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e2
 363 e1) \to (ex2 C (\lambda (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c2
 364 c1))))))))) (\lambda (c2: C).(\lambda (e2: C).(\lambda (H: (drop1 PNil c2
 365 e2)).(\lambda (e1: C).(\lambda (H0: (csubc g e2 e1)).(let H1 \def (match H in
 366 drop1 return (\lambda (p: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda
 367 (_: (drop1 p c c0)).((eq PList p PNil) \to ((eq C c c2) \to ((eq C c0 e2) \to
 368 (ex2 C (\lambda (c1: C).(drop1 PNil c1 e1)) (\lambda (c1: C).(csubc g c2
 369 c1)))))))))) with [(drop1_nil c) \Rightarrow (\lambda (_: (eq PList PNil
 370 PNil)).(\lambda (H2: (eq C c c2)).(\lambda (H3: (eq C c e2)).(eq_ind C c2
 371 (\lambda (c0: C).((eq C c0 e2) \to (ex2 C (\lambda (c1: C).(drop1 PNil c1
 372 e1)) (\lambda (c1: C).(csubc g c2 c1))))) (\lambda (H4: (eq C c2 e2)).(eq_ind
 373 C e2 (\lambda (c0: C).(ex2 C (\lambda (c1: C).(drop1 PNil c1 e1)) (\lambda
 374 (c1: C).(csubc g c0 c1)))) (let H5 \def (eq_ind_r C e2 (\lambda (c0:
 375 C).(csubc g c0 e1)) H0 c2 H4) in (eq_ind C c2 (\lambda (c0: C).(ex2 C
 376 (\lambda (c1: C).(drop1 PNil c1 e1)) (\lambda (c1: C).(csubc g c0 c1))))
 377 (ex_intro2 C (\lambda (c1: C).(drop1 PNil c1 e1)) (\lambda (c1: C).(csubc g
 378 c2 c1)) e1 (drop1_nil e1) H5) e2 H4)) c2 (sym_eq C c2 e2 H4))) c (sym_eq C c
 379 c2 H2) H3)))) | (drop1_cons c1 c0 h d H1 c3 hds0 H2) \Rightarrow (\lambda
 380 (H3: (eq PList (PCons h d hds0) PNil)).(\lambda (H4: (eq C c1 c2)).(\lambda
 381 (H5: (eq C c3 e2)).((let H6 \def (eq_ind PList (PCons h d hds0) (\lambda (e:
 382 PList).(match e in PList return (\lambda (_: PList).Prop) with [PNil
 383 \Rightarrow False | (PCons _ _ _) \Rightarrow True])) I PNil H3) in
 384 (False_ind ((eq C c1 c2) \to ((eq C c3 e2) \to ((drop h d c1 c0) \to ((drop1
 385 hds0 c0 c3) \to (ex2 C (\lambda (c4: C).(drop1 PNil c4 e1)) (\lambda (c4:
 386 C).(csubc g c2 c4))))))) H6)) H4 H5 H1 H2))))]) in (H1 (refl_equal PList
 387 PNil) (refl_equal C c2) (refl_equal C e2)))))))) (\lambda (n: nat).(\lambda
 388 (n0: nat).(\lambda (p: PList).(\lambda (H: ((\forall (c2: C).(\forall (e2:
 389 C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C (\lambda
 390 (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c2 c1)))))))))).(\lambda
 391 (c2: C).(\lambda (e2: C).(\lambda (H0: (drop1 (PCons n n0 p) c2 e2)).(\lambda
 392 (e1: C).(\lambda (H1: (csubc g e2 e1)).(let H2 \def (match H0 in drop1 return
 393 (\lambda (p0: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda (_: (drop1 p0
 394 c c0)).((eq PList p0 (PCons n n0 p)) \to ((eq C c c2) \to ((eq C c0 e2) \to
 395 (ex2 C (\lambda (c1: C).(drop1 (PCons n n0 p) c1 e1)) (\lambda (c1: C).(csubc
 396 g c2 c1)))))))))) with [(drop1_nil c) \Rightarrow (\lambda (H2: (eq PList
 397 PNil (PCons n n0 p))).(\lambda (H3: (eq C c c2)).(\lambda (H4: (eq C c
 398 e2)).((let H5 \def (eq_ind PList PNil (\lambda (e: PList).(match e in PList
 399 return (\lambda (_: PList).Prop) with [PNil \Rightarrow True | (PCons _ _ _)
 400 \Rightarrow False])) I (PCons n n0 p) H2) in (False_ind ((eq C c c2) \to ((eq
 401 C c e2) \to (ex2 C (\lambda (c1: C).(drop1 (PCons n n0 p) c1 e1)) (\lambda
 402 (c1: C).(csubc g c2 c1))))) H5)) H3 H4)))) | (drop1_cons c1 c0 h d H2 c3 hds0
 403 H3) \Rightarrow (\lambda (H4: (eq PList (PCons h d hds0) (PCons n n0
 404 p))).(\lambda (H5: (eq C c1 c2)).(\lambda (H6: (eq C c3 e2)).((let H7 \def
 405 (f_equal PList PList (\lambda (e: PList).(match e in PList return (\lambda
 406 (_: PList).PList) with [PNil \Rightarrow hds0 | (PCons _ _ p0) \Rightarrow
 407 p0])) (PCons h d hds0) (PCons n n0 p) H4) in ((let H8 \def (f_equal PList nat
 408 (\lambda (e: PList).(match e in PList return (\lambda (_: PList).nat) with
 409 [PNil \Rightarrow d | (PCons _ n1 _) \Rightarrow n1])) (PCons h d hds0)
 410 (PCons n n0 p) H4) in ((let H9 \def (f_equal PList nat (\lambda (e:
 411 PList).(match e in PList return (\lambda (_: PList).nat) with [PNil
 412 \Rightarrow h | (PCons n1 _ _) \Rightarrow n1])) (PCons h d hds0) (PCons n n0
 413 p) H4) in (eq_ind nat n (\lambda (n1: nat).((eq nat d n0) \to ((eq PList hds0
 414 p) \to ((eq C c1 c2) \to ((eq C c3 e2) \to ((drop n1 d c1 c0) \to ((drop1
 415 hds0 c0 c3) \to (ex2 C (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1))
 416 (\lambda (c4: C).(csubc g c2 c4)))))))))) (\lambda (H10: (eq nat d
 417 n0)).(eq_ind nat n0 (\lambda (n1: nat).((eq PList hds0 p) \to ((eq C c1 c2)
 418 \to ((eq C c3 e2) \to ((drop n n1 c1 c0) \to ((drop1 hds0 c0 c3) \to (ex2 C
 419 (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1)) (\lambda (c4: C).(csubc g c2
 420 c4))))))))) (\lambda (H11: (eq PList hds0 p)).(eq_ind PList p (\lambda (p0:
 421 PList).((eq C c1 c2) \to ((eq C c3 e2) \to ((drop n n0 c1 c0) \to ((drop1 p0
 422 c0 c3) \to (ex2 C (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1)) (\lambda
 423 (c4: C).(csubc g c2 c4)))))))) (\lambda (H12: (eq C c1 c2)).(eq_ind C c2
 424 (\lambda (c: C).((eq C c3 e2) \to ((drop n n0 c c0) \to ((drop1 p c0 c3) \to
 425 (ex2 C (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1)) (\lambda (c4: C).(csubc
 426 g c2 c4))))))) (\lambda (H13: (eq C c3 e2)).(eq_ind C e2 (\lambda (c:
 427 C).((drop n n0 c2 c0) \to ((drop1 p c0 c) \to (ex2 C (\lambda (c4: C).(drop1
 428 (PCons n n0 p) c4 e1)) (\lambda (c4: C).(csubc g c2 c4)))))) (\lambda (H14:
 429 (drop n n0 c2 c0)).(\lambda (H15: (drop1 p c0 e2)).(let H_x \def (H c0 e2 H15
 430 e1 H1) in (let H16 \def H_x in (ex2_ind C (\lambda (c4: C).(drop1 p c4 e1))
 431 (\lambda (c4: C).(csubc g c0 c4)) (ex2 C (\lambda (c4: C).(drop1 (PCons n n0
 432 p) c4 e1)) (\lambda (c4: C).(csubc g c2 c4))) (\lambda (x: C).(\lambda (H17:
 433 (drop1 p x e1)).(\lambda (H18: (csubc g c0 x)).(let H_x0 \def
 434 (drop_csubc_trans g c2 c0 n0 n H14 x H18) in (let H19 \def H_x0 in (ex2_ind C
 435 (\lambda (c4: C).(drop n n0 c4 x)) (\lambda (c4: C).(csubc g c2 c4)) (ex2 C
 436 (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1)) (\lambda (c4: C).(csubc g c2
 437 c4))) (\lambda (x0: C).(\lambda (H20: (drop n n0 x0 x)).(\lambda (H21: (csubc
 438 g c2 x0)).(ex_intro2 C (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1))
 439 (\lambda (c4: C).(csubc g c2 c4)) x0 (drop1_cons x0 x n n0 H20 e1 p H17)
 440 H21)))) H19)))))) H16))))) c3 (sym_eq C c3 e2 H13))) c1 (sym_eq C c1 c2
 441 H12))) hds0 (sym_eq PList hds0 p H11))) d (sym_eq nat d n0 H10))) h (sym_eq
 442 nat h n H9))) H8)) H7)) H5 H6 H2 H3))))]) in (H2 (refl_equal PList (PCons n
 443 n0 p)) (refl_equal C c2) (refl_equal C e2)))))))))))) hds)).
 444
 445 theorem csubc_drop1_conf_rev:
 446  \forall (g: G).(\forall (hds: PList).(\forall (c2: C).(\forall (e2:
 447 C).((drop1 hds c2 e2) \to (\forall (e1: C).((csubc g e1 e2) \to (ex2 C
 448 (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(csubc g c1 c2)))))))))
 449 \def
 450  \lambda (g: G).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
 451 (c2: C).(\forall (e2: C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e1
 452 e2) \to (ex2 C (\lambda (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c1
 453 c2))))))))) (\lambda (c2: C).(\lambda (e2: C).(\lambda (H: (drop1 PNil c2
 454 e2)).(\lambda (e1: C).(\lambda (H0: (csubc g e1 e2)).(let H1 \def (match H in
 455 drop1 return (\lambda (p: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda
 456 (_: (drop1 p c c0)).((eq PList p PNil) \to ((eq C c c2) \to ((eq C c0 e2) \to
 457 (ex2 C (\lambda (c1: C).(drop1 PNil c1 e1)) (\lambda (c1: C).(csubc g c1
 458 c2)))))))))) with [(drop1_nil c) \Rightarrow (\lambda (_: (eq PList PNil
 459 PNil)).(\lambda (H2: (eq C c c2)).(\lambda (H3: (eq C c e2)).(eq_ind C c2
 460 (\lambda (c0: C).((eq C c0 e2) \to (ex2 C (\lambda (c1: C).(drop1 PNil c1
 461 e1)) (\lambda (c1: C).(csubc g c1 c2))))) (\lambda (H4: (eq C c2 e2)).(eq_ind
 462 C e2 (\lambda (c0: C).(ex2 C (\lambda (c1: C).(drop1 PNil c1 e1)) (\lambda
 463 (c1: C).(csubc g c1 c0)))) (let H5 \def (eq_ind_r C e2 (\lambda (c0:
 464 C).(csubc g e1 c0)) H0 c2 H4) in (eq_ind C c2 (\lambda (c0: C).(ex2 C
 465 (\lambda (c1: C).(drop1 PNil c1 e1)) (\lambda (c1: C).(csubc g c1 c0))))
 466 (ex_intro2 C (\lambda (c1: C).(drop1 PNil c1 e1)) (\lambda (c1: C).(csubc g
 467 c1 c2)) e1 (drop1_nil e1) H5) e2 H4)) c2 (sym_eq C c2 e2 H4))) c (sym_eq C c
 468 c2 H2) H3)))) | (drop1_cons c1 c0 h d H1 c3 hds0 H2) \Rightarrow (\lambda
 469 (H3: (eq PList (PCons h d hds0) PNil)).(\lambda (H4: (eq C c1 c2)).(\lambda
 470 (H5: (eq C c3 e2)).((let H6 \def (eq_ind PList (PCons h d hds0) (\lambda (e:
 471 PList).(match e in PList return (\lambda (_: PList).Prop) with [PNil
 472 \Rightarrow False | (PCons _ _ _) \Rightarrow True])) I PNil H3) in
 473 (False_ind ((eq C c1 c2) \to ((eq C c3 e2) \to ((drop h d c1 c0) \to ((drop1
 474 hds0 c0 c3) \to (ex2 C (\lambda (c4: C).(drop1 PNil c4 e1)) (\lambda (c4:
 475 C).(csubc g c4 c2))))))) H6)) H4 H5 H1 H2))))]) in (H1 (refl_equal PList
 476 PNil) (refl_equal C c2) (refl_equal C e2)))))))) (\lambda (n: nat).(\lambda
 477 (n0: nat).(\lambda (p: PList).(\lambda (H: ((\forall (c2: C).(\forall (e2:
 478 C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e1 e2) \to (ex2 C (\lambda
 479 (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c1 c2)))))))))).(\lambda
 480 (c2: C).(\lambda (e2: C).(\lambda (H0: (drop1 (PCons n n0 p) c2 e2)).(\lambda
 481 (e1: C).(\lambda (H1: (csubc g e1 e2)).(let H2 \def (match H0 in drop1 return
 482 (\lambda (p0: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda (_: (drop1 p0
 483 c c0)).((eq PList p0 (PCons n n0 p)) \to ((eq C c c2) \to ((eq C c0 e2) \to
 484 (ex2 C (\lambda (c1: C).(drop1 (PCons n n0 p) c1 e1)) (\lambda (c1: C).(csubc
 485 g c1 c2)))))))))) with [(drop1_nil c) \Rightarrow (\lambda (H2: (eq PList
 486 PNil (PCons n n0 p))).(\lambda (H3: (eq C c c2)).(\lambda (H4: (eq C c
 487 e2)).((let H5 \def (eq_ind PList PNil (\lambda (e: PList).(match e in PList
 488 return (\lambda (_: PList).Prop) with [PNil \Rightarrow True | (PCons _ _ _)
 489 \Rightarrow False])) I (PCons n n0 p) H2) in (False_ind ((eq C c c2) \to ((eq
 490 C c e2) \to (ex2 C (\lambda (c1: C).(drop1 (PCons n n0 p) c1 e1)) (\lambda
 491 (c1: C).(csubc g c1 c2))))) H5)) H3 H4)))) | (drop1_cons c1 c0 h d H2 c3 hds0
 492 H3) \Rightarrow (\lambda (H4: (eq PList (PCons h d hds0) (PCons n n0
 493 p))).(\lambda (H5: (eq C c1 c2)).(\lambda (H6: (eq C c3 e2)).((let H7 \def
 494 (f_equal PList PList (\lambda (e: PList).(match e in PList return (\lambda
 495 (_: PList).PList) with [PNil \Rightarrow hds0 | (PCons _ _ p0) \Rightarrow
 496 p0])) (PCons h d hds0) (PCons n n0 p) H4) in ((let H8 \def (f_equal PList nat
 497 (\lambda (e: PList).(match e in PList return (\lambda (_: PList).nat) with
 498 [PNil \Rightarrow d | (PCons _ n1 _) \Rightarrow n1])) (PCons h d hds0)
 499 (PCons n n0 p) H4) in ((let H9 \def (f_equal PList nat (\lambda (e:
 500 PList).(match e in PList return (\lambda (_: PList).nat) with [PNil
 501 \Rightarrow h | (PCons n1 _ _) \Rightarrow n1])) (PCons h d hds0) (PCons n n0
 502 p) H4) in (eq_ind nat n (\lambda (n1: nat).((eq nat d n0) \to ((eq PList hds0
 503 p) \to ((eq C c1 c2) \to ((eq C c3 e2) \to ((drop n1 d c1 c0) \to ((drop1
 504 hds0 c0 c3) \to (ex2 C (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1))
 505 (\lambda (c4: C).(csubc g c4 c2)))))))))) (\lambda (H10: (eq nat d
 506 n0)).(eq_ind nat n0 (\lambda (n1: nat).((eq PList hds0 p) \to ((eq C c1 c2)
 507 \to ((eq C c3 e2) \to ((drop n n1 c1 c0) \to ((drop1 hds0 c0 c3) \to (ex2 C
 508 (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1)) (\lambda (c4: C).(csubc g c4
 509 c2))))))))) (\lambda (H11: (eq PList hds0 p)).(eq_ind PList p (\lambda (p0:
 510 PList).((eq C c1 c2) \to ((eq C c3 e2) \to ((drop n n0 c1 c0) \to ((drop1 p0
 511 c0 c3) \to (ex2 C (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1)) (\lambda
 512 (c4: C).(csubc g c4 c2)))))))) (\lambda (H12: (eq C c1 c2)).(eq_ind C c2
 513 (\lambda (c: C).((eq C c3 e2) \to ((drop n n0 c c0) \to ((drop1 p c0 c3) \to
 514 (ex2 C (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1)) (\lambda (c4: C).(csubc
 515 g c4 c2))))))) (\lambda (H13: (eq C c3 e2)).(eq_ind C e2 (\lambda (c:
 516 C).((drop n n0 c2 c0) \to ((drop1 p c0 c) \to (ex2 C (\lambda (c4: C).(drop1
 517 (PCons n n0 p) c4 e1)) (\lambda (c4: C).(csubc g c4 c2)))))) (\lambda (H14:
 518 (drop n n0 c2 c0)).(\lambda (H15: (drop1 p c0 e2)).(let H_x \def (H c0 e2 H15
 519 e1 H1) in (let H16 \def H_x in (ex2_ind C (\lambda (c4: C).(drop1 p c4 e1))
 520 (\lambda (c4: C).(csubc g c4 c0)) (ex2 C (\lambda (c4: C).(drop1 (PCons n n0
 521 p) c4 e1)) (\lambda (c4: C).(csubc g c4 c2))) (\lambda (x: C).(\lambda (H17:
 522 (drop1 p x e1)).(\lambda (H18: (csubc g x c0)).(let H_x0 \def
 523 (csubc_drop_conf_rev g c2 c0 n0 n H14 x H18) in (let H19 \def H_x0 in
 524 (ex2_ind C (\lambda (c4: C).(drop n n0 c4 x)) (\lambda (c4: C).(csubc g c4
 525 c2)) (ex2 C (\lambda (c4: C).(drop1 (PCons n n0 p) c4 e1)) (\lambda (c4:
 526 C).(csubc g c4 c2))) (\lambda (x0: C).(\lambda (H20: (drop n n0 x0
 527 x)).(\lambda (H21: (csubc g x0 c2)).(ex_intro2 C (\lambda (c4: C).(drop1
 528 (PCons n n0 p) c4 e1)) (\lambda (c4: C).(csubc g c4 c2)) x0 (drop1_cons x0 x
 529 n n0 H20 e1 p H17) H21)))) H19)))))) H16))))) c3 (sym_eq C c3 e2 H13))) c1
 530 (sym_eq C c1 c2 H12))) hds0 (sym_eq PList hds0 p H11))) d (sym_eq nat d n0
 531 H10))) h (sym_eq nat h n H9))) H8)) H7)) H5 H6 H2 H3))))]) in (H2 (refl_equal
 532 PList (PCons n n0 p)) (refl_equal C c2) (refl_equal C e2)))))))))))) hds)).
 533
 534 theorem drop1_ceqc_trans:
 535  \forall (g: G).(\forall (hds: PList).(\forall (c2: C).(\forall (e2:
 536 C).((drop1 hds c2 e2) \to (\forall (e1: C).((ceqc g e2 e1) \to (ex2 C
 537 (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(ceqc g c2 c1)))))))))
 538 \def
 539  \lambda (g: G).(\lambda (hds: PList).(\lambda (c2: C).(\lambda (e2:
 540 C).(\lambda (H: (drop1 hds c2 e2)).(\lambda (e1: C).(\lambda (H0: (ceqc g e2
 541 e1)).(let H1 \def H0 in (or_ind (csubc g e2 e1) (csubc g e1 e2) (ex2 C
 542 (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(ceqc g c2 c1)))
 543 (\lambda (H2: (csubc g e2 e1)).(let H_x \def (drop1_csubc_trans g hds c2 e2 H
 544 e1 H2) in (let H3 \def H_x in (ex2_ind C (\lambda (c1: C).(drop1 hds c1 e1))
 545 (\lambda (c1: C).(csubc g c2 c1)) (ex2 C (\lambda (c1: C).(drop1 hds c1 e1))
 546 (\lambda (c1: C).(ceqc g c2 c1))) (\lambda (x: C).(\lambda (H4: (drop1 hds x
 547 e1)).(\lambda (H5: (csubc g c2 x)).(ex_intro2 C (\lambda (c1: C).(drop1 hds
 548 c1 e1)) (\lambda (c1: C).(ceqc g c2 c1)) x H4 (or_introl (csubc g c2 x)
 549 (csubc g x c2) H5))))) H3)))) (\lambda (H2: (csubc g e1 e2)).(let H_x \def
 550 (csubc_drop1_conf_rev g hds c2 e2 H e1 H2) in (let H3 \def H_x in (ex2_ind C
 551 (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(csubc g c1 c2)) (ex2 C
 552 (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(ceqc g c2 c1)))
 553 (\lambda (x: C).(\lambda (H4: (drop1 hds x e1)).(\lambda (H5: (csubc g x
 554 c2)).(ex_intro2 C (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(ceqc
 555 g c2 c1)) x H4 (or_intror (csubc g c2 x) (csubc g x c2) H5))))) H3))))
 556 H1)))))))).
 557
 558 axiom sc3_ceqc_trans:
 559  \forall (g: G).(\forall (a: A).(\forall (vs: TList).(\forall (c1:
 560 C).(\forall (t: T).((sc3 g a c1 (THeads (Flat Appl) vs t)) \to (\forall (c2:
 561 C).((ceqc g c2 c1) \to (sc3 g a c2 (THeads (Flat Appl) vs t)))))))))
 562 .
 563