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 lemma 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 H1 \def (getl_gen_all c1 (CHead d1 (Bind
  33 b1) v1) i H0) in (ex2_ind C (\lambda (e: C).(drop i O c1 e)) (\lambda (e:
  34 C).(clear e (CHead d1 (Bind b1) v1))) (ex2_3 B C T (\lambda (_: B).(\lambda
  35 (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
  36 C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind b2) v2)))))) (\lambda (x:
  37 C).(\lambda (H2: (drop i O c1 x)).(\lambda (H3: (clear x (CHead d1 (Bind b1)
  38 v1))).(let H_x \def (csubv_drop_conf c1 c2 H x i H2) in (let H4 \def H_x in
  39 (ex2_ind C (\lambda (e2: C).(csubv x e2)) (\lambda (e2: C).(drop i O c2 e2))
  40 (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
  41 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead
  42 d2 (Bind b2) v2)))))) (\lambda (x0: C).(\lambda (H5: (csubv x x0)).(\lambda
  43 (H6: (drop i O c2 x0)).(let H_x0 \def (csubv_clear_conf x x0 H5 b1 d1 v1 H3)
  44 in (let H7 \def H_x0 in (ex2_3_ind B C T (\lambda (_: B).(\lambda (d2:
  45 C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
  46 C).(\lambda (v2: T).(clear x0 (CHead d2 (Bind b2) v2))))) (ex2_3 B C T
  47 (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda
  48 (b2: B).(\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind b2)
  49 v2)))))) (\lambda (x1: B).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H8:
  50 (csubv d1 x2)).(\lambda (H9: (clear x0 (CHead x2 (Bind x1) x3))).(ex2_3_intro
  51 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))))
  52 (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind
  53 b2) v2))))) x1 x2 x3 H8 (getl_intro i c2 (CHead x2 (Bind x1) x3) x0 H6
  54 H9))))))) H7)))))) H4)))))) H1))))))))).
  55
  56 lemma csubv_getl_conf_void:
  57  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1:
  58 C).(\forall (v1: T).(\forall (i: nat).((getl i c1 (CHead d1 (Bind Void) v1))
  59 \to (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2:
  60 C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind Void) v2)))))))))))
  61 \def
  62  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(\lambda (d1:
  63 C).(\lambda (v1: T).(\lambda (i: nat).(\lambda (H0: (getl i c1 (CHead d1
  64 (Bind Void) v1))).(let H1 \def (getl_gen_all c1 (CHead d1 (Bind Void) v1) i
  65 H0) in (ex2_ind C (\lambda (e: C).(drop i O c1 e)) (\lambda (e: C).(clear e
  66 (CHead d1 (Bind Void) v1))) (ex2_2 C T (\lambda (d2: C).(\lambda (_:
  67 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2
  68 (Bind Void) v2))))) (\lambda (x: C).(\lambda (H2: (drop i O c1 x)).(\lambda
  69 (H3: (clear x (CHead d1 (Bind Void) v1))).(let H_x \def (csubv_drop_conf c1
  70 c2 H x i H2) in (let H4 \def H_x in (ex2_ind C (\lambda (e2: C).(csubv x e2))
  71 (\lambda (e2: C).(drop i O c2 e2)) (ex2_2 C T (\lambda (d2: C).(\lambda (_:
  72 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2
  73 (Bind Void) v2))))) (\lambda (x0: C).(\lambda (H5: (csubv x x0)).(\lambda
  74 (H6: (drop i O c2 x0)).(let H_x0 \def (csubv_clear_conf_void x x0 H5 d1 v1
  75 H3) in (let H7 \def H_x0 in (ex2_2_ind C T (\lambda (d2: C).(\lambda (_:
  76 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear x0 (CHead d2
  77 (Bind Void) v2)))) (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1
  78 d2))) (\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind Void)
  79 v2))))) (\lambda (x1: C).(\lambda (x2: T).(\lambda (H8: (csubv d1
  80 x1)).(\lambda (H9: (clear x0 (CHead x1 (Bind Void) x2))).(ex2_2_intro C T
  81 (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
  82 (v2: T).(getl i c2 (CHead d2 (Bind Void) v2)))) x1 x2 H8 (getl_intro i c2
  83 (CHead x1 (Bind Void) x2) x0 H6 H9)))))) H7)))))) H4)))))) H1)))))))).
  84