matita/matita/contribs/lambdadelta/basic_1A/ex2/props.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_1A/ex2/defs.ma".
  18
  19 include "basic_1A/nf2/defs.ma".
  20
  21 include "basic_1A/pr2/fwd.ma".
  22
  23 include "basic_1A/arity/fwd.ma".
  24
  25 lemma ex2_nf2:
  26  nf2 ex2_c ex2_t
  27 \def
  28  \lambda (t2: T).(\lambda (H: (pr2 (CSort O) (THead (Flat Appl) (TSort O)
  29 (TSort O)) t2)).(let H0 \def (pr2_gen_appl (CSort O) (TSort O) (TSort O) t2
  30 H) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
  31 (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 (CSort O) (TSort
  32 O) u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 (CSort O) (TSort O) t3))))
  33 (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
  34 T).(eq T (TSort O) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda
  35 (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
  36 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
  37 T).(pr2 (CSort O) (TSort O) u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda
  38 (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead (CSort O)
  39 (Bind b) u) z1 t3)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_:
  40 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
  41 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
  42 T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O) (THead (Bind b) y1
  43 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2:
  44 T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind b) y2 (THead (Flat
  45 Appl) (lift (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
  46 (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 (CSort O) (TSort
  47 O) u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
  48 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CSort O) y1 y2))))))) (\lambda (b:
  49 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
  50 (y2: T).(pr2 (CHead (CSort O) (Bind b) y2) z1 z2)))))))) (eq T (THead (Flat
  51 Appl) (TSort O) (TSort O)) t2) (\lambda (H1: (ex3_2 T T (\lambda (u2:
  52 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
  53 T).(\lambda (_: T).(pr2 (CSort O) (TSort O) u2))) (\lambda (_: T).(\lambda
  54 (t3: T).(pr2 (CSort O) (TSort O) t3))))).(ex3_2_ind T T (\lambda (u2:
  55 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
  56 T).(\lambda (_: T).(pr2 (CSort O) (TSort O) u2))) (\lambda (_: T).(\lambda
  57 (t3: T).(pr2 (CSort O) (TSort O) t3))) (eq T (THead (Flat Appl) (TSort O)
  58 (TSort O)) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H2: (eq T t2
  59 (THead (Flat Appl) x0 x1))).(\lambda (H3: (pr2 (CSort O) (TSort O)
  60 x0)).(\lambda (H4: (pr2 (CSort O) (TSort O) x1)).(let H5 \def (eq_ind T x1
  61 (\lambda (t: T).(eq T t2 (THead (Flat Appl) x0 t))) H2 (TSort O)
  62 (pr2_gen_sort (CSort O) x1 O H4)) in (let H6 \def (eq_ind T x0 (\lambda (t:
  63 T).(eq T t2 (THead (Flat Appl) t (TSort O)))) H5 (TSort O) (pr2_gen_sort
  64 (CSort O) x0 O H3)) in (eq_ind_r T (THead (Flat Appl) (TSort O) (TSort O))
  65 (\lambda (t: T).(eq T (THead (Flat Appl) (TSort O) (TSort O)) t)) (refl_equal
  66 T (THead (Flat Appl) (TSort O) (TSort O))) t2 H6)))))))) H1)) (\lambda (H1:
  67 (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
  68 T).(eq T (TSort O) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda
  69 (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
  70 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
  71 T).(pr2 (CSort O) (TSort O) u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda
  72 (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead (CSort O)
  73 (Bind b) u) z1 t3))))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1:
  74 T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O) (THead (Bind Abst) y1
  75 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
  76 T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
  77 T).(\lambda (u2: T).(\lambda (_: T).(pr2 (CSort O) (TSort O) u2))))) (\lambda
  78 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b:
  79 B).(\forall (u: T).(pr2 (CHead (CSort O) (Bind b) u) z1 t3))))))) (eq T
  80 (THead (Flat Appl) (TSort O) (TSort O)) t2) (\lambda (x0: T).(\lambda (x1:
  81 T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (H2: (eq T (TSort O) (THead
  82 (Bind Abst) x0 x1))).(\lambda (H3: (eq T t2 (THead (Bind Abbr) x2
  83 x3))).(\lambda (H4: (pr2 (CSort O) (TSort O) x2)).(\lambda (_: ((\forall (b:
  84 B).(\forall (u: T).(pr2 (CHead (CSort O) (Bind b) u) x1 x3))))).(let H6 \def
  85 (eq_ind T x2 (\lambda (t: T).(eq T t2 (THead (Bind Abbr) t x3))) H3 (TSort O)
  86 (pr2_gen_sort (CSort O) x2 O H4)) in (eq_ind_r T (THead (Bind Abbr) (TSort O)
  87 x3) (\lambda (t: T).(eq T (THead (Flat Appl) (TSort O) (TSort O)) t)) (let H7
  88 \def (eq_ind T (TSort O) (\lambda (ee: T).(match ee with [(TSort _)
  89 \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
  90 False])) I (THead (Bind Abst) x0 x1) H2) in (False_ind (eq T (THead (Flat
  91 Appl) (TSort O) (TSort O)) (THead (Bind Abbr) (TSort O) x3)) H7)) t2
  92 H6)))))))))) H1)) (\lambda (H1: (ex6_6 B T T T T T (\lambda (b: B).(\lambda
  93 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not
  94 (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
  95 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O) (THead
  96 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
  97 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
  98 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
  99 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
 100 (_: T).(pr2 (CSort O) (TSort O) u2))))))) (\lambda (_: B).(\lambda (y1:
 101 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2
 102 (CSort O) y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
 103 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead (CSort O)
 104 (Bind b) y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda
 105 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not
 106 (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
 107 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O) (THead
 108 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
 109 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
 110 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
 111 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
 112 (_: T).(pr2 (CSort O) (TSort O) u2))))))) (\lambda (_: B).(\lambda (y1:
 113 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2
 114 (CSort O) y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
 115 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead (CSort O)
 116 (Bind b) y2) z1 z2))))))) (eq T (THead (Flat Appl) (TSort O) (TSort O)) t2)
 117 (\lambda (x0: B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda
 118 (x4: T).(\lambda (x5: T).(\lambda (_: (not (eq B x0 Abst))).(\lambda (H3: (eq
 119 T (TSort O) (THead (Bind x0) x1 x2))).(\lambda (H4: (eq T t2 (THead (Bind x0)
 120 x5 (THead (Flat Appl) (lift (S O) O x4) x3)))).(\lambda (H5: (pr2 (CSort O)
 121 (TSort O) x4)).(\lambda (H6: (pr2 (CSort O) x1 x5)).(\lambda (_: (pr2 (CHead
 122 (CSort O) (Bind x0) x5) x2 x3)).(let H_y \def (pr2_gen_csort x1 x5 O H6) in
 123 (let H8 \def (eq_ind T x4 (\lambda (t: T).(eq T t2 (THead (Bind x0) x5 (THead
 124 (Flat Appl) (lift (S O) O t) x3)))) H4 (TSort O) (pr2_gen_sort (CSort O) x4 O
 125 H5)) in (eq_ind_r T (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O
 126 (TSort O)) x3)) (\lambda (t: T).(eq T (THead (Flat Appl) (TSort O) (TSort O))
 127 t)) (let H9 \def (eq_ind T (TSort O) (\lambda (ee: T).(match ee with [(TSort
 128 _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
 129 False])) I (THead (Bind x0) x1 x2) H3) in (False_ind (eq T (THead (Flat Appl)
 130 (TSort O) (TSort O)) (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O
 131 (TSort O)) x3))) H9)) t2 H8))))))))))))))) H1)) H0))).
 132
 133 lemma ex2_arity:
 134  \forall (g: G).(\forall (a: A).((arity g ex2_c ex2_t a) \to (\forall (P:
 135 Prop).P)))
 136 \def
 137  \lambda (g: G).(\lambda (a: A).(\lambda (H: (arity g (CSort O) (THead (Flat
 138 Appl) (TSort O) (TSort O)) a)).(\lambda (P: Prop).(let H0 \def
 139 (arity_gen_appl g (CSort O) (TSort O) (TSort O) a H) in (ex2_ind A (\lambda
 140 (a1: A).(arity g (CSort O) (TSort O) a1)) (\lambda (a1: A).(arity g (CSort O)
 141 (TSort O) (AHead a1 a))) P (\lambda (x: A).(\lambda (_: (arity g (CSort O)
 142 (TSort O) x)).(\lambda (H2: (arity g (CSort O) (TSort O) (AHead x a))).(let
 143 H_x \def (leq_gen_head1 g x a (ASort O O) (arity_gen_sort g (CSort O) O
 144 (AHead x a) H2)) in (let H3 \def H_x in (ex3_2_ind A A (\lambda (a3:
 145 A).(\lambda (_: A).(leq g x a3))) (\lambda (_: A).(\lambda (a4: A).(leq g a
 146 a4))) (\lambda (a3: A).(\lambda (a4: A).(eq A (ASort O O) (AHead a3 a4)))) P
 147 (\lambda (x0: A).(\lambda (x1: A).(\lambda (_: (leq g x x0)).(\lambda (_:
 148 (leq g a x1)).(\lambda (H6: (eq A (ASort O O) (AHead x0 x1))).(let H7 \def
 149 (eq_ind A (ASort O O) (\lambda (ee: A).(match ee with [(ASort _ _)
 150 \Rightarrow True | (AHead _ _) \Rightarrow False])) I (AHead x0 x1) H6) in
 151 (False_ind P H7))))))) H3)))))) H0))))).
 152