1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "LambdaDelta-1/T/defs.ma".
19 theorem not_abbr_abst:
22 \lambda (H: (eq B Abbr Abst)).(let H0 \def (eq_ind B Abbr (\lambda (ee:
23 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow True |
24 Abst \Rightarrow False | Void \Rightarrow False])) I Abst H) in (False_ind
27 theorem not_void_abst:
30 \lambda (H: (eq B Void Abst)).(let H0 \def (eq_ind B Void (\lambda (ee:
31 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
32 Abst \Rightarrow False | Void \Rightarrow True])) I Abst H) in (False_ind
35 theorem not_abbr_void:
38 \lambda (H: (eq B Abbr Void)).(let H0 \def (eq_ind B Abbr (\lambda (ee:
39 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow True |
40 Abst \Rightarrow False | Void \Rightarrow False])) I Void H) in (False_ind
43 theorem not_abst_void:
46 \lambda (H: (eq B Abst Void)).(let H0 \def (eq_ind B Abst (\lambda (ee:
47 B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
48 Abst \Rightarrow True | Void \Rightarrow False])) I Void H) in (False_ind
52 \forall (k: K).(\forall (v: T).(\forall (t: T).((eq T (THead k v t) t) \to
53 (\forall (P: Prop).P))))
55 \lambda (k: K).(\lambda (v: T).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq
56 T (THead k v t0) t0) \to (\forall (P: Prop).P))) (\lambda (n: nat).(\lambda
57 (H: (eq T (THead k v (TSort n)) (TSort n))).(\lambda (P: Prop).(let H0 \def
58 (eq_ind T (THead k v (TSort n)) (\lambda (ee: T).(match ee in T return
59 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
60 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H) in
61 (False_ind P H0))))) (\lambda (n: nat).(\lambda (H: (eq T (THead k v (TLRef
62 n)) (TLRef n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead k v (TLRef
63 n)) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
64 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
65 \Rightarrow True])) I (TLRef n) H) in (False_ind P H0))))) (\lambda (k0:
66 K).(\lambda (t0: T).(\lambda (_: (((eq T (THead k v t0) t0) \to (\forall (P:
67 Prop).P)))).(\lambda (t1: T).(\lambda (H0: (((eq T (THead k v t1) t1) \to
68 (\forall (P: Prop).P)))).(\lambda (H1: (eq T (THead k v (THead k0 t0 t1))
69 (THead k0 t0 t1))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e:
70 T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k |
71 (TLRef _) \Rightarrow k | (THead k1 _ _) \Rightarrow k1])) (THead k v (THead
72 k0 t0 t1)) (THead k0 t0 t1) H1) in ((let H3 \def (f_equal T T (\lambda (e:
73 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v |
74 (TLRef _) \Rightarrow v | (THead _ t2 _) \Rightarrow t2])) (THead k v (THead
75 k0 t0 t1)) (THead k0 t0 t1) H1) in ((let H4 \def (f_equal T T (\lambda (e:
76 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead
77 k0 t0 t1) | (TLRef _) \Rightarrow (THead k0 t0 t1) | (THead _ _ t2)
78 \Rightarrow t2])) (THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) in
79 (\lambda (H5: (eq T v t0)).(\lambda (H6: (eq K k k0)).(let H7 \def (eq_ind T
80 v (\lambda (t2: T).((eq T (THead k t2 t1) t1) \to (\forall (P0: Prop).P0)))
81 H0 t0 H5) in (let H8 \def (eq_ind K k (\lambda (k1: K).((eq T (THead k1 t0
82 t1) t1) \to (\forall (P0: Prop).P0))) H7 k0 H6) in (H8 H4 P)))))) H3))
86 \forall (t: T).(lt O (tweight t))
88 \lambda (t: T).(T_ind (\lambda (t0: T).(lt O (tweight t0))) (\lambda (_:
89 nat).(le_n (S O))) (\lambda (_: nat).(le_n (S O))) (\lambda (_: K).(\lambda
90 (t0: T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O
91 (tweight t1))).(le_S (S O) (plus (tweight t0) (tweight t1)) (le_plus_trans (S
92 O) (tweight t0) (tweight t1) H))))))) t).