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 theorem 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).(let TMP_3 \def (\lambda (p:
  25 PList).(\forall (c2: C).(\forall (e2: C).((drop1 p c2 e2) \to (\forall (e1:
  26 C).((csubc g e2 e1) \to (let TMP_1 \def (\lambda (c1: C).(drop1 p c1 e1)) in
  27 (let TMP_2 \def (\lambda (c1: C).(csubc g c2 c1)) in (ex2 C TMP_1
  28 TMP_2))))))))) in (let TMP_8 \def (\lambda (c2: C).(\lambda (e2: C).(\lambda
  29 (H: (drop1 PNil c2 e2)).(\lambda (e1: C).(\lambda (H0: (csubc g e2 e1)).(let
  30 H_y \def (drop1_gen_pnil c2 e2 H) in (let TMP_4 \def (\lambda (c: C).(csubc g
  31 c e1)) in (let H1 \def (eq_ind_r C e2 TMP_4 H0 c2 H_y) in (let TMP_5 \def
  32 (\lambda (c1: C).(drop1 PNil c1 e1)) in (let TMP_6 \def (\lambda (c1:
  33 C).(csubc g c2 c1)) in (let TMP_7 \def (drop1_nil e1) in (ex_intro2 C TMP_5
  34 TMP_6 e1 TMP_7 H1)))))))))))) in (let TMP_34 \def (\lambda (n: nat).(\lambda
  35 (n0: nat).(\lambda (p: PList).(\lambda (H: ((\forall (c2: C).(\forall (e2:
  36 C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C (\lambda
  37 (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c2 c1)))))))))).(\lambda
  38 (c2: C).(\lambda (e2: C).(\lambda (H0: (drop1 (PCons n n0 p) c2 e2)).(\lambda
  39 (e1: C).(\lambda (H1: (csubc g e2 e1)).(let H_x \def (drop1_gen_pcons c2 e2 p
  40 n n0 H0) in (let H2 \def H_x in (let TMP_9 \def (\lambda (c3: C).(drop n n0
  41 c2 c3)) in (let TMP_10 \def (\lambda (c3: C).(drop1 p c3 e2)) in (let TMP_12
  42 \def (\lambda (c1: C).(let TMP_11 \def (PCons n n0 p) in (drop1 TMP_11 c1
  43 e1))) in (let TMP_13 \def (\lambda (c1: C).(csubc g c2 c1)) in (let TMP_14
  44 \def (ex2 C TMP_12 TMP_13) in (let TMP_33 \def (\lambda (x: C).(\lambda (H3:
  45 (drop n n0 c2 x)).(\lambda (H4: (drop1 p x e2)).(let H_x0 \def (H x e2 H4 e1
  46 H1) in (let H5 \def H_x0 in (let TMP_15 \def (\lambda (c1: C).(drop1 p c1
  47 e1)) in (let TMP_16 \def (\lambda (c1: C).(csubc g x c1)) in (let TMP_18 \def
  48 (\lambda (c1: C).(let TMP_17 \def (PCons n n0 p) in (drop1 TMP_17 c1 e1))) in
  49 (let TMP_19 \def (\lambda (c1: C).(csubc g c2 c1)) in (let TMP_20 \def (ex2 C
  50 TMP_18 TMP_19) in (let TMP_32 \def (\lambda (x0: C).(\lambda (H6: (drop1 p x0
  51 e1)).(\lambda (H7: (csubc g x x0)).(let H_x1 \def (drop_csubc_trans g c2 x n0
  52 n H3 x0 H7) in (let H8 \def H_x1 in (let TMP_21 \def (\lambda (c1: C).(drop n
  53 n0 c1 x0)) in (let TMP_22 \def (\lambda (c1: C).(csubc g c2 c1)) in (let
  54 TMP_24 \def (\lambda (c1: C).(let TMP_23 \def (PCons n n0 p) in (drop1 TMP_23
  55 c1 e1))) in (let TMP_25 \def (\lambda (c1: C).(csubc g c2 c1)) in (let TMP_26
  56 \def (ex2 C TMP_24 TMP_25) in (let TMP_31 \def (\lambda (x1: C).(\lambda (H9:
  57 (drop n n0 x1 x0)).(\lambda (H10: (csubc g c2 x1)).(let TMP_28 \def (\lambda
  58 (c1: C).(let TMP_27 \def (PCons n n0 p) in (drop1 TMP_27 c1 e1))) in (let
  59 TMP_29 \def (\lambda (c1: C).(csubc g c2 c1)) in (let TMP_30 \def (drop1_cons
  60 x1 x0 n n0 H9 e1 p H6) in (ex_intro2 C TMP_28 TMP_29 x1 TMP_30 H10))))))) in
  61 (ex2_ind C TMP_21 TMP_22 TMP_26 TMP_31 H8)))))))))))) in (ex2_ind C TMP_15
  62 TMP_16 TMP_20 TMP_32 H5)))))))))))) in (ex2_ind C TMP_9 TMP_10 TMP_14 TMP_33
  63 H2)))))))))))))))))) in (PList_ind TMP_3 TMP_8 TMP_34 hds))))).
  64
  65 theorem csubc_drop1_conf_rev:
  66  \forall (g: G).(\forall (hds: PList).(\forall (c2: C).(\forall (e2:
  67 C).((drop1 hds c2 e2) \to (\forall (e1: C).((csubc g e1 e2) \to (ex2 C
  68 (\lambda (c1: C).(drop1 hds c1 e1)) (\lambda (c1: C).(csubc g c1 c2)))))))))
  69 \def
  70  \lambda (g: G).(\lambda (hds: PList).(let TMP_3 \def (\lambda (p:
  71 PList).(\forall (c2: C).(\forall (e2: C).((drop1 p c2 e2) \to (\forall (e1:
  72 C).((csubc g e1 e2) \to (let TMP_1 \def (\lambda (c1: C).(drop1 p c1 e1)) in
  73 (let TMP_2 \def (\lambda (c1: C).(csubc g c1 c2)) in (ex2 C TMP_1
  74 TMP_2))))))))) in (let TMP_8 \def (\lambda (c2: C).(\lambda (e2: C).(\lambda
  75 (H: (drop1 PNil c2 e2)).(\lambda (e1: C).(\lambda (H0: (csubc g e1 e2)).(let
  76 H_y \def (drop1_gen_pnil c2 e2 H) in (let TMP_4 \def (\lambda (c: C).(csubc g
  77 e1 c)) in (let H1 \def (eq_ind_r C e2 TMP_4 H0 c2 H_y) in (let TMP_5 \def
  78 (\lambda (c1: C).(drop1 PNil c1 e1)) in (let TMP_6 \def (\lambda (c1:
  79 C).(csubc g c1 c2)) in (let TMP_7 \def (drop1_nil e1) in (ex_intro2 C TMP_5
  80 TMP_6 e1 TMP_7 H1)))))))))))) in (let TMP_34 \def (\lambda (n: nat).(\lambda
  81 (n0: nat).(\lambda (p: PList).(\lambda (H: ((\forall (c2: C).(\forall (e2:
  82 C).((drop1 p c2 e2) \to (\forall (e1: C).((csubc g e1 e2) \to (ex2 C (\lambda
  83 (c1: C).(drop1 p c1 e1)) (\lambda (c1: C).(csubc g c1 c2)))))))))).(\lambda
  84 (c2: C).(\lambda (e2: C).(\lambda (H0: (drop1 (PCons n n0 p) c2 e2)).(\lambda
  85 (e1: C).(\lambda (H1: (csubc g e1 e2)).(let H_x \def (drop1_gen_pcons c2 e2 p
  86 n n0 H0) in (let H2 \def H_x in (let TMP_9 \def (\lambda (c3: C).(drop n n0
  87 c2 c3)) in (let TMP_10 \def (\lambda (c3: C).(drop1 p c3 e2)) in (let TMP_12
  88 \def (\lambda (c1: C).(let TMP_11 \def (PCons n n0 p) in (drop1 TMP_11 c1
  89 e1))) in (let TMP_13 \def (\lambda (c1: C).(csubc g c1 c2)) in (let TMP_14
  90 \def (ex2 C TMP_12 TMP_13) in (let TMP_33 \def (\lambda (x: C).(\lambda (H3:
  91 (drop n n0 c2 x)).(\lambda (H4: (drop1 p x e2)).(let H_x0 \def (H x e2 H4 e1
  92 H1) in (let H5 \def H_x0 in (let TMP_15 \def (\lambda (c1: C).(drop1 p c1
  93 e1)) in (let TMP_16 \def (\lambda (c1: C).(csubc g c1 x)) in (let TMP_18 \def
  94 (\lambda (c1: C).(let TMP_17 \def (PCons n n0 p) in (drop1 TMP_17 c1 e1))) in
  95 (let TMP_19 \def (\lambda (c1: C).(csubc g c1 c2)) in (let TMP_20 \def (ex2 C
  96 TMP_18 TMP_19) in (let TMP_32 \def (\lambda (x0: C).(\lambda (H6: (drop1 p x0
  97 e1)).(\lambda (H7: (csubc g x0 x)).(let H_x1 \def (csubc_drop_conf_rev g c2 x
  98 n0 n H3 x0 H7) in (let H8 \def H_x1 in (let TMP_21 \def (\lambda (c1:
  99 C).(drop n n0 c1 x0)) in (let TMP_22 \def (\lambda (c1: C).(csubc g c1 c2))
 100 in (let TMP_24 \def (\lambda (c1: C).(let TMP_23 \def (PCons n n0 p) in
 101 (drop1 TMP_23 c1 e1))) in (let TMP_25 \def (\lambda (c1: C).(csubc g c1 c2))
 102 in (let TMP_26 \def (ex2 C TMP_24 TMP_25) in (let TMP_31 \def (\lambda (x1:
 103 C).(\lambda (H9: (drop n n0 x1 x0)).(\lambda (H10: (csubc g x1 c2)).(let
 104 TMP_28 \def (\lambda (c1: C).(let TMP_27 \def (PCons n n0 p) in (drop1 TMP_27
 105 c1 e1))) in (let TMP_29 \def (\lambda (c1: C).(csubc g c1 c2)) in (let TMP_30
 106 \def (drop1_cons x1 x0 n n0 H9 e1 p H6) in (ex_intro2 C TMP_28 TMP_29 x1
 107 TMP_30 H10))))))) in (ex2_ind C TMP_21 TMP_22 TMP_26 TMP_31 H8)))))))))))) in
 108 (ex2_ind C TMP_15 TMP_16 TMP_20 TMP_32 H5)))))))))))) in (ex2_ind C TMP_9
 109 TMP_10 TMP_14 TMP_33 H2)))))))))))))))))) in (PList_ind TMP_3 TMP_8 TMP_34
 110 hds))))).
 111