matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare3.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
  18
  19 include "theory.ma".
  20
  21 inductive sort: T \to Prop \def
  22 | sort_sort: \forall (n: nat).(sort (TSort n))
  23 | sort_abst: \forall (u: T).((sort u) \to (\forall (t: T).((sort t) \to (sort
  24 (THead (Bind Abst) u t))))).
  25
  26 theorem sort_nf2:
  27  \forall (t: T).((sort t) \to (\forall (c: C).(nf2 c t)))
  28 \def
  29  \lambda (t: T).(\lambda (H: (sort t)).(sort_ind (\lambda (t0: T).(\forall
  30 (c: C).(nf2 c t0))) (\lambda (n: nat).(\lambda (c: C).(nf2_sort c n)))
  31 (\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1: ((\forall (c: C).(nf2 c
  32 u)))).(\lambda (t0: T).(\lambda (_: (sort t0)).(\lambda (H3: ((\forall (c:
  33 C).(nf2 c t0)))).(\lambda (c: C).(let H_y \def (H3 (CHead c (Bind Abst) u))
  34 in (nf2_abst_shift c u (H1 c) t0 H_y))))))))) t H)).
  35
  36 theorem sort_pc3:
  37  \forall (t1: T).((sort t1) \to (\forall (t2: T).((sort t2) \to (\forall (c:
  38 C).((pc3 c t1 t2) \to (eq T t1 t2))))))
  39 \def
  40  \lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda (t: T).(\forall
  41 (t2: T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t t2))))))
  42 (\lambda (n: nat).(\lambda (t2: T).(\lambda (H0: (sort t2)).(sort_ind
  43 (\lambda (t: T).(\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n)
  44 t)))) (\lambda (n0: nat).(\lambda (c: C).(\lambda (H1: (pc3 c (TSort n)
  45 (TSort n0))).(eq_ind nat n (\lambda (n1: nat).(eq T (TSort n) (TSort n1)))
  46 (refl_equal T (TSort n)) n0 (pc3_gen_sort c n n0 H1))))) (\lambda (u:
  47 T).(\lambda (_: (sort u)).(\lambda (_: ((\forall (c: C).((pc3 c (TSort n) u)
  48 \to (eq T (TSort n) u))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda
  49 (_: ((\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n) t))))).(\lambda
  50 (c: C).(\lambda (H5: (pc3 c (TSort n) (THead (Bind Abst) u
  51 t))).(pc3_gen_sort_abst c u t n H5 (eq T (TSort n) (THead (Bind Abst) u
  52 t))))))))))) t2 H0)))) (\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1:
  53 ((\forall (t2: T).((sort t2) \to (\forall (c: C).((pc3 c u t2) \to (eq T u
  54 t2))))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3: ((\forall (t2:
  55 T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t
  56 t2))))))).(\lambda (t2: T).(\lambda (H4: (sort t2)).(sort_ind (\lambda (t0:
  57 T).(\forall (c: C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind
  58 Abst) u t) t0)))) (\lambda (n: nat).(\lambda (c: C).(\lambda (H5: (pc3 c
  59 (THead (Bind Abst) u t) (TSort n))).(pc3_gen_sort_abst c u t n (pc3_s c
  60 (TSort n) (THead (Bind Abst) u t) H5) (eq T (THead (Bind Abst) u t) (TSort
  61 n)))))) (\lambda (u0: T).(\lambda (H5: (sort u0)).(\lambda (_: ((\forall (c:
  62 C).((pc3 c (THead (Bind Abst) u t) u0) \to (eq T (THead (Bind Abst) u t)
  63 u0))))).(\lambda (t0: T).(\lambda (H7: (sort t0)).(\lambda (_: ((\forall (c:
  64 C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind Abst) u t)
  65 t0))))).(\lambda (c: C).(\lambda (H9: (pc3 c (THead (Bind Abst) u t) (THead
  66 (Bind Abst) u0 t0))).(and_ind (pc3 c u u0) (\forall (b: B).(\forall (u1:
  67 T).(pc3 (CHead c (Bind b) u1) t t0))) (eq T (THead (Bind Abst) u t) (THead
  68 (Bind Abst) u0 t0)) (\lambda (H10: (pc3 c u u0)).(\lambda (H11: ((\forall (b:
  69 B).(\forall (u1: T).(pc3 (CHead c (Bind b) u1) t t0))))).(let H_y \def (H11
  70 Abbr u) in (let H_y0 \def (H1 u0 H5 c H10) in (let H_y1 \def (H3 t0 H7 (CHead
  71 c (Bind Abbr) u) H_y) in (let H12 \def (eq_ind_r T t0 (\lambda (t3: T).(pc3
  72 (CHead c (Bind Abbr) u) t t3)) H_y t H_y1) in (let H13 \def (eq_ind_r T t0
  73 (\lambda (t3: T).(sort t3)) H7 t H_y1) in (eq_ind T t (\lambda (t3: T).(eq T
  74 (THead (Bind Abst) u t) (THead (Bind Abst) u0 t3))) (let H14 \def (eq_ind_r T
  75 u0 (\lambda (t3: T).(pc3 c u t3)) H10 u H_y0) in (let H15 \def (eq_ind_r T u0
  76 (\lambda (t3: T).(sort t3)) H5 u H_y0) in (eq_ind T u (\lambda (t3: T).(eq T
  77 (THead (Bind Abst) u t) (THead (Bind Abst) t3 t))) (refl_equal T (THead (Bind
  78 Abst) u t)) u0 H_y0))) t0 H_y1)))))))) (pc3_gen_abst c u u0 t t0 H9))))))))))
  79 t2 H4))))))))) t1 H)).
  80
  81 theorem sort_correct:
  82  \forall (g: G).(\forall (t1: T).((sort t1) \to (\forall (c: C).(ex3 T
  83 (\lambda (t2: T).(tau0 g c t1 t2)) (\lambda (t2: T).(ty3 g c t1 t2)) (\lambda
  84 (t2: T).(sort t2))))))
  85 \def
  86  \lambda (g: G).(\lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda
  87 (t: T).(\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2:
  88 T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2))))) (\lambda (n: nat).(\lambda
  89 (c: C).(ex3_intro T (\lambda (t2: T).(tau0 g c (TSort n) t2)) (\lambda (t2:
  90 T).(ty3 g c (TSort n) t2)) (\lambda (t2: T).(sort t2)) (TSort (next g n))
  91 (tau0_sort g c n) (ty3_sort g c n) (sort_sort (next g n))))) (\lambda (u:
  92 T).(\lambda (H0: (sort u)).(\lambda (H1: ((\forall (c: C).(ex3 T (\lambda
  93 (t2: T).(tau0 g c u t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2:
  94 T).(sort t2)))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3:
  95 ((\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2:
  96 T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2)))))).(\lambda (c: C).(let H_x
  97 \def (H1 c) in (let H4 \def H_x in (ex3_ind T (\lambda (t2: T).(tau0 g c u
  98 t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2: T).(sort t2)) (ex3 T
  99 (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(ty3
 100 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) (\lambda (x0:
 101 T).(\lambda (_: (tau0 g c u x0)).(\lambda (H6: (ty3 g c u x0)).(\lambda (_:
 102 (sort x0)).(let H_x0 \def (H3 (CHead c (Bind Abst) u)) in (let H8 \def H_x0
 103 in (ex3_ind T (\lambda (t2: T).(tau0 g (CHead c (Bind Abst) u) t t2))
 104 (\lambda (t2: T).(ty3 g (CHead c (Bind Abst) u) t t2)) (\lambda (t2: T).(sort
 105 t2)) (ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda
 106 (t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2)))
 107 (\lambda (x1: T).(\lambda (H9: (tau0 g (CHead c (Bind Abst) u) t
 108 x1)).(\lambda (H10: (ty3 g (CHead c (Bind Abst) u) t x1)).(\lambda (H11:
 109 (sort x1)).(ex_ind T (\lambda (t0: T).(ty3 g (CHead c (Bind Abst) u) x1 t0))
 110 (ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2:
 111 T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2)))
 112 (\lambda (x: T).(\lambda (H12: (ty3 g (CHead c (Bind Abst) u) x1
 113 x)).(ex3_intro T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2))
 114 (\lambda (t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort
 115 t2)) (THead (Bind Abst) u x1) (tau0_bind g Abst c u t x1 H9) (ty3_bind g c u
 116 x0 H6 Abst t x1 H10 x H12) (sort_abst u H0 x1 H11)))) (ty3_correct g (CHead c
 117 (Bind Abst) u) t x1 H10)))))) H8))))))) H4)))))))))) t1 H))).
 118