matita/matita/contribs/lambdadelta/basic_1/csubv/getl.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/csubv/clear.ma".
  18
  19 include "basic_1/csubv/drop.ma".
  20
  21 include "basic_1/getl/fwd.ma".
  22
  23 theorem csubv_getl_conf:
  24  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1:
  25 B).(\forall (d1: C).(\forall (v1: T).(\forall (i: nat).((getl i c1 (CHead d1
  26 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
  27 T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(getl
  28 i c2 (CHead d2 (Bind b2) v2)))))))))))))
  29 \def
  30  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(\lambda (b1:
  31 B).(\lambda (d1: C).(\lambda (v1: T).(\lambda (i: nat).(\lambda (H0: (getl i
  32 c1 (CHead d1 (Bind b1) v1))).(let TMP_1 \def (Bind b1) in (let TMP_2 \def
  33 (CHead d1 TMP_1 v1) in (let H1 \def (getl_gen_all c1 TMP_2 i H0) in (let
  34 TMP_3 \def (\lambda (e: C).(drop i O c1 e)) in (let TMP_6 \def (\lambda (e:
  35 C).(let TMP_4 \def (Bind b1) in (let TMP_5 \def (CHead d1 TMP_4 v1) in (clear
  36 e TMP_5)))) in (let TMP_7 \def (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
  37 T).(csubv d1 d2)))) in (let TMP_10 \def (\lambda (b2: B).(\lambda (d2:
  38 C).(\lambda (v2: T).(let TMP_8 \def (Bind b2) in (let TMP_9 \def (CHead d2
  39 TMP_8 v2) in (getl i c2 TMP_9)))))) in (let TMP_11 \def (ex2_3 B C T TMP_7
  40 TMP_10) in (let TMP_37 \def (\lambda (x: C).(\lambda (H2: (drop i O c1
  41 x)).(\lambda (H3: (clear x (CHead d1 (Bind b1) v1))).(let H_x \def
  42 (csubv_drop_conf c1 c2 H x i H2) in (let H4 \def H_x in (let TMP_12 \def
  43 (\lambda (e2: C).(csubv x e2)) in (let TMP_13 \def (\lambda (e2: C).(drop i O
  44 c2 e2)) in (let TMP_14 \def (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
  45 T).(csubv d1 d2)))) in (let TMP_17 \def (\lambda (b2: B).(\lambda (d2:
  46 C).(\lambda (v2: T).(let TMP_15 \def (Bind b2) in (let TMP_16 \def (CHead d2
  47 TMP_15 v2) in (getl i c2 TMP_16)))))) in (let TMP_18 \def (ex2_3 B C T TMP_14
  48 TMP_17) in (let TMP_36 \def (\lambda (x0: C).(\lambda (H5: (csubv x
  49 x0)).(\lambda (H6: (drop i O c2 x0)).(let H_x0 \def (csubv_clear_conf x x0 H5
  50 b1 d1 v1 H3) in (let H7 \def H_x0 in (let TMP_19 \def (\lambda (_:
  51 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) in (let TMP_22 \def
  52 (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let TMP_20 \def (Bind b2)
  53 in (let TMP_21 \def (CHead d2 TMP_20 v2) in (clear x0 TMP_21)))))) in (let
  54 TMP_23 \def (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))))
  55 in (let TMP_26 \def (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let
  56 TMP_24 \def (Bind b2) in (let TMP_25 \def (CHead d2 TMP_24 v2) in (getl i c2
  57 TMP_25)))))) in (let TMP_27 \def (ex2_3 B C T TMP_23 TMP_26) in (let TMP_35
  58 \def (\lambda (x1: B).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H8: (csubv
  59 d1 x2)).(\lambda (H9: (clear x0 (CHead x2 (Bind x1) x3))).(let TMP_28 \def
  60 (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) in (let
  61 TMP_31 \def (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let TMP_29
  62 \def (Bind b2) in (let TMP_30 \def (CHead d2 TMP_29 v2) in (getl i c2
  63 TMP_30)))))) in (let TMP_32 \def (Bind x1) in (let TMP_33 \def (CHead x2
  64 TMP_32 x3) in (let TMP_34 \def (getl_intro i c2 TMP_33 x0 H6 H9) in
  65 (ex2_3_intro B C T TMP_28 TMP_31 x1 x2 x3 H8 TMP_34))))))))))) in (ex2_3_ind
  66 B C T TMP_19 TMP_22 TMP_27 TMP_35 H7)))))))))))) in (ex2_ind C TMP_12 TMP_13
  67 TMP_18 TMP_36 H4)))))))))))) in (ex2_ind C TMP_3 TMP_6 TMP_11 TMP_37
  68 H1))))))))))))))))).
  69
  70 theorem csubv_getl_conf_void:
  71  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1:
  72 C).(\forall (v1: T).(\forall (i: nat).((getl i c1 (CHead d1 (Bind Void) v1))
  73 \to (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2:
  74 C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind Void) v2)))))))))))
  75 \def
  76  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(\lambda (d1:
  77 C).(\lambda (v1: T).(\lambda (i: nat).(\lambda (H0: (getl i c1 (CHead d1
  78 (Bind Void) v1))).(let TMP_1 \def (Bind Void) in (let TMP_2 \def (CHead d1
  79 TMP_1 v1) in (let H1 \def (getl_gen_all c1 TMP_2 i H0) in (let TMP_3 \def
  80 (\lambda (e: C).(drop i O c1 e)) in (let TMP_6 \def (\lambda (e: C).(let
  81 TMP_4 \def (Bind Void) in (let TMP_5 \def (CHead d1 TMP_4 v1) in (clear e
  82 TMP_5)))) in (let TMP_7 \def (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))
  83 in (let TMP_10 \def (\lambda (d2: C).(\lambda (v2: T).(let TMP_8 \def (Bind
  84 Void) in (let TMP_9 \def (CHead d2 TMP_8 v2) in (getl i c2 TMP_9))))) in (let
  85 TMP_11 \def (ex2_2 C T TMP_7 TMP_10) in (let TMP_37 \def (\lambda (x:
  86 C).(\lambda (H2: (drop i O c1 x)).(\lambda (H3: (clear x (CHead d1 (Bind
  87 Void) v1))).(let H_x \def (csubv_drop_conf c1 c2 H x i H2) in (let H4 \def
  88 H_x in (let TMP_12 \def (\lambda (e2: C).(csubv x e2)) in (let TMP_13 \def
  89 (\lambda (e2: C).(drop i O c2 e2)) in (let TMP_14 \def (\lambda (d2:
  90 C).(\lambda (_: T).(csubv d1 d2))) in (let TMP_17 \def (\lambda (d2:
  91 C).(\lambda (v2: T).(let TMP_15 \def (Bind Void) in (let TMP_16 \def (CHead
  92 d2 TMP_15 v2) in (getl i c2 TMP_16))))) in (let TMP_18 \def (ex2_2 C T TMP_14
  93 TMP_17) in (let TMP_36 \def (\lambda (x0: C).(\lambda (H5: (csubv x
  94 x0)).(\lambda (H6: (drop i O c2 x0)).(let H_x0 \def (csubv_clear_conf_void x
  95 x0 H5 d1 v1 H3) in (let H7 \def H_x0 in (let TMP_19 \def (\lambda (d2:
  96 C).(\lambda (_: T).(csubv d1 d2))) in (let TMP_22 \def (\lambda (d2:
  97 C).(\lambda (v2: T).(let TMP_20 \def (Bind Void) in (let TMP_21 \def (CHead
  98 d2 TMP_20 v2) in (clear x0 TMP_21))))) in (let TMP_23 \def (\lambda (d2:
  99 C).(\lambda (_: T).(csubv d1 d2))) in (let TMP_26 \def (\lambda (d2:
 100 C).(\lambda (v2: T).(let TMP_24 \def (Bind Void) in (let TMP_25 \def (CHead
 101 d2 TMP_24 v2) in (getl i c2 TMP_25))))) in (let TMP_27 \def (ex2_2 C T TMP_23
 102 TMP_26) in (let TMP_35 \def (\lambda (x1: C).(\lambda (x2: T).(\lambda (H8:
 103 (csubv d1 x1)).(\lambda (H9: (clear x0 (CHead x1 (Bind Void) x2))).(let
 104 TMP_28 \def (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) in (let TMP_31
 105 \def (\lambda (d2: C).(\lambda (v2: T).(let TMP_29 \def (Bind Void) in (let
 106 TMP_30 \def (CHead d2 TMP_29 v2) in (getl i c2 TMP_30))))) in (let TMP_32
 107 \def (Bind Void) in (let TMP_33 \def (CHead x1 TMP_32 x2) in (let TMP_34 \def
 108 (getl_intro i c2 TMP_33 x0 H6 H9) in (ex2_2_intro C T TMP_28 TMP_31 x1 x2 H8
 109 TMP_34)))))))))) in (ex2_2_ind C T TMP_19 TMP_22 TMP_27 TMP_35 H7))))))))))))
 110 in (ex2_ind C TMP_12 TMP_13 TMP_18 TMP_36 H4)))))))))))) in (ex2_ind C TMP_3
 111 TMP_6 TMP_11 TMP_37 H1)))))))))))))))).
 112