matita/matita/contribs/lambdadelta/basic_1/csubc/drop1.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_1/csubc/drop.ma".
  18
  19 lemma drop1_csubc_trans:
  20  \forall (g: G).(\forall (hds: PList).(\forall (c2: C).(\forall (e2:
  21 C).((drop1 hds c2 e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C
  22 (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(csubc g c2 c1)))))))))
  23 \def
  24  \lambda (g: G).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
  25 (c2: C).(\forall (e2: C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e2
  26 e1) \to (ex2 C (\lambda (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c2
  27 c1))))))))) (\lambda (c2: C).(\lambda (e2: C).(\lambda (H: (drop1 PNil c2
  28 e2)).(\lambda (e1: C).(\lambda (H0: (csubc g e2 e1)).(let H_y \def
  29 (drop1_gen_pnil c2 e2 H) in (let H1 \def (eq_ind_r C e2 (\lambda (c:
  30 C).(csubc g c e1)) H0 c2 H_y) in (ex_intro2 C (\lambda (c1: C).(drop1 PNil c1
  31 e1)) (\lambda (c1: C).(csubc g c2 c1)) e1 (drop1_nil e1) H1)))))))) (\lambda
  32 (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: ((\forall (c2:
  33 C).(\forall (e2: C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e2 e1)
  34 \to (ex2 C (\lambda (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c2
  35 c1)))))))))).(\lambda (c2: C).(\lambda (e2: C).(\lambda (H0: (drop1 (PCons n
  36 n0 p) c2 e2)).(\lambda (e1: C).(\lambda (H1: (csubc g e2 e1)).(let H_x \def
  37 (drop1_gen_pcons c2 e2 p n n0 H0) in (let H2 \def H_x in (ex2_ind C (\lambda
  38 (c3: C).(drop n n0 c2 c3)) (\lambda (c3: C).(drop1 p c3 e2)) (ex2 C (\lambda
  39 (c1: C).(drop1 (PCons n n0 p) c1 e1)) (\lambda (c1: C).(csubc g c2 c1)))
  40 (\lambda (x: C).(\lambda (H3: (drop n n0 c2 x)).(\lambda (H4: (drop1 p x
  41 e2)).(let H_x0 \def (H x e2 H4 e1 H1) in (let H5 \def H_x0 in (ex2_ind C
  42 (\lambda (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g x c1)) (ex2 C
  43 (\lambda (c1: C).(drop1 (PCons n n0 p) c1 e1)) (\lambda (c1: C).(csubc g c2
  44 c1))) (\lambda (x0: C).(\lambda (H6: (drop1 p x0 e1)).(\lambda (H7: (csubc g
  45 x x0)).(let H_x1 \def (drop_csubc_trans g c2 x n0 n H3 x0 H7) in (let H8 \def
  46 H_x1 in (ex2_ind C (\lambda (c1: C).(drop n n0 c1 x0)) (\lambda (c1:
  47 C).(csubc g c2 c1)) (ex2 C (\lambda (c1: C).(drop1 (PCons n n0 p) c1 e1))
  48 (\lambda (c1: C).(csubc g c2 c1))) (\lambda (x1: C).(\lambda (H9: (drop n n0
  49 x1 x0)).(\lambda (H10: (csubc g c2 x1)).(ex_intro2 C (\lambda (c1: C).(drop1
  50 (PCons n n0 p) c1 e1)) (\lambda (c1: C).(csubc g c2 c1)) x1 (drop1_cons x1 x0
  51 n n0 H9 e1 p H6) H10)))) H8)))))) H5)))))) H2)))))))))))) hds)).
  52
  53 lemma csubc_drop1_conf_rev:
  54  \forall (g: G).(\forall (hds: PList).(\forall (c2: C).(\forall (e2:
  55 C).((drop1 hds c2 e2) \to (\forall (e1: C).((csubc g e1 e2) \to (ex2 C
  56 (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(csubc g c1 c2)))))))))
  57 \def
  58  \lambda (g: G).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
  59 (c2: C).(\forall (e2: C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e1
  60 e2) \to (ex2 C (\lambda (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c1
  61 c2))))))))) (\lambda (c2: C).(\lambda (e2: C).(\lambda (H: (drop1 PNil c2
  62 e2)).(\lambda (e1: C).(\lambda (H0: (csubc g e1 e2)).(let H_y \def
  63 (drop1_gen_pnil c2 e2 H) in (let H1 \def (eq_ind_r C e2 (\lambda (c:
  64 C).(csubc g e1 c)) H0 c2 H_y) in (ex_intro2 C (\lambda (c1: C).(drop1 PNil c1
  65 e1)) (\lambda (c1: C).(csubc g c1 c2)) e1 (drop1_nil e1) H1)))))))) (\lambda
  66 (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: ((\forall (c2:
  67 C).(\forall (e2: C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e1 e2)
  68 \to (ex2 C (\lambda (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c1
  69 c2)))))))))).(\lambda (c2: C).(\lambda (e2: C).(\lambda (H0: (drop1 (PCons n
  70 n0 p) c2 e2)).(\lambda (e1: C).(\lambda (H1: (csubc g e1 e2)).(let H_x \def
  71 (drop1_gen_pcons c2 e2 p n n0 H0) in (let H2 \def H_x in (ex2_ind C (\lambda
  72 (c3: C).(drop n n0 c2 c3)) (\lambda (c3: C).(drop1 p c3 e2)) (ex2 C (\lambda
  73 (c1: C).(drop1 (PCons n n0 p) c1 e1)) (\lambda (c1: C).(csubc g c1 c2)))
  74 (\lambda (x: C).(\lambda (H3: (drop n n0 c2 x)).(\lambda (H4: (drop1 p x
  75 e2)).(let H_x0 \def (H x e2 H4 e1 H1) in (let H5 \def H_x0 in (ex2_ind C
  76 (\lambda (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c1 x)) (ex2 C
  77 (\lambda (c1: C).(drop1 (PCons n n0 p) c1 e1)) (\lambda (c1: C).(csubc g c1
  78 c2))) (\lambda (x0: C).(\lambda (H6: (drop1 p x0 e1)).(\lambda (H7: (csubc g
  79 x0 x)).(let H_x1 \def (csubc_drop_conf_rev g c2 x n0 n H3 x0 H7) in (let H8
  80 \def H_x1 in (ex2_ind C (\lambda (c1: C).(drop n n0 c1 x0)) (\lambda (c1:
  81 C).(csubc g c1 c2)) (ex2 C (\lambda (c1: C).(drop1 (PCons n n0 p) c1 e1))
  82 (\lambda (c1: C).(csubc g c1 c2))) (\lambda (x1: C).(\lambda (H9: (drop n n0
  83 x1 x0)).(\lambda (H10: (csubc g x1 c2)).(ex_intro2 C (\lambda (c1: C).(drop1
  84 (PCons n n0 p) c1 e1)) (\lambda (c1: C).(csubc g c1 c2)) x1 (drop1_cons x1 x0
  85 n n0 H9 e1 p H6) H10)))) H8)))))) H5)))))) H2)))))))))))) hds)).
  86