]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_1A/T/props.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / basic_1A / T / 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/T/fwd.ma".
18
19 lemma not_abbr_abst:
20  not (eq B Abbr Abst)
21 \def
22  \lambda (H: (eq B Abbr Abst)).(let H0 \def (eq_ind B Abbr (\lambda (ee: 
23 B).(match ee with [Abbr \Rightarrow True | Abst \Rightarrow False | Void 
24 \Rightarrow False])) I Abst H) in (False_ind False H0)).
25
26 lemma not_void_abst:
27  not (eq B Void Abst)
28 \def
29  \lambda (H: (eq B Void Abst)).(let H0 \def (eq_ind B Void (\lambda (ee: 
30 B).(match ee with [Abbr \Rightarrow False | Abst \Rightarrow False | Void 
31 \Rightarrow True])) I Abst H) in (False_ind False H0)).
32
33 lemma not_abbr_void:
34  not (eq B Abbr Void)
35 \def
36  \lambda (H: (eq B Abbr Void)).(let H0 \def (eq_ind B Abbr (\lambda (ee: 
37 B).(match ee with [Abbr \Rightarrow True | Abst \Rightarrow False | Void 
38 \Rightarrow False])) I Void H) in (False_ind False H0)).
39
40 lemma not_abst_void:
41  not (eq B Abst Void)
42 \def
43  \lambda (H: (eq B Abst Void)).(let H0 \def (eq_ind B Abst (\lambda (ee: 
44 B).(match ee with [Abbr \Rightarrow False | Abst \Rightarrow True | Void 
45 \Rightarrow False])) I Void H) in (False_ind False H0)).
46
47 lemma tweight_lt:
48  \forall (t: T).(lt O (tweight t))
49 \def
50  \lambda (t: T).(T_ind (\lambda (t0: T).(lt O (tweight t0))) (\lambda (_: 
51 nat).(le_n (S O))) (\lambda (_: nat).(le_n (S O))) (\lambda (_: K).(\lambda 
52 (t0: T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O 
53 (tweight t1))).(le_S (S O) (plus (tweight t0) (tweight t1)) (le_plus_trans (S 
54 O) (tweight t0) (tweight t1) H))))))) t).
55
56 lemma tle_r:
57  \forall (t: T).(tle t t)
58 \def
59  \lambda (t: T).(T_ind (\lambda (t0: T).(le (tweight t0) (tweight t0))) 
60 (\lambda (_: nat).(le_n (S O))) (\lambda (_: nat).(le_n (S O))) (\lambda (_: 
61 K).(\lambda (t0: T).(\lambda (_: (le (tweight t0) (tweight t0))).(\lambda 
62 (t1: T).(\lambda (_: (le (tweight t1) (tweight t1))).(le_n (S (plus (tweight 
63 t0) (tweight t1))))))))) t).
64