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 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd".
19 include "nf2/defs.ma".
21 include "pr2/clen.ma".
26 \forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
27 (CHead d (Bind Abbr) u)) \to ((nf2 c (TLRef i)) \to (\forall (P: Prop).P))))))
29 \lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
30 (H: (getl i c (CHead d (Bind Abbr) u))).(\lambda (H0: ((\forall (t2: T).((pr2
31 c (TLRef i) t2) \to (eq T (TLRef i) t2))))).(\lambda (P:
32 Prop).(lift_gen_lref_false (S i) O i (le_O_n i) (le_n (plus O (S i))) u (H0
33 (lift (S i) O u) (pr2_delta c d u i H (TLRef i) (TLRef i) (pr0_refl (TLRef
34 i)) (lift (S i) O u) (subst0_lref u i))) P))))))).
37 \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Bind Abst) u
38 t)) \to (land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)))))
40 \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: ((\forall (t2:
41 T).((pr2 c (THead (Bind Abst) u t) t2) \to (eq T (THead (Bind Abst) u t)
42 t2))))).(conj (\forall (t2: T).((pr2 c u t2) \to (eq T u t2))) (\forall (t2:
43 T).((pr2 (CHead c (Bind Abst) u) t t2) \to (eq T t t2))) (\lambda (t2:
44 T).(\lambda (H0: (pr2 c u t2)).(let H1 \def (f_equal T T (\lambda (e:
45 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u |
46 (TLRef _) \Rightarrow u | (THead _ t0 _) \Rightarrow t0])) (THead (Bind Abst)
47 u t) (THead (Bind Abst) t2 t) (H (THead (Bind Abst) t2 t) (pr2_head_1 c u t2
48 H0 (Bind Abst) t))) in (let H2 \def (eq_ind_r T t2 (\lambda (t0: T).(pr2 c u
49 t0)) H0 u H1) in (eq_ind T u (\lambda (t0: T).(eq T u t0)) (refl_equal T u)
50 t2 H1))))) (\lambda (t2: T).(\lambda (H0: (pr2 (CHead c (Bind Abst) u) t
51 t2)).(let H1 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda
52 (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _
53 _ t0) \Rightarrow t0])) (THead (Bind Abst) u t) (THead (Bind Abst) u t2) (H
54 (THead (Bind Abst) u t2) (let H_y \def (pr2_gen_cbind Abst c u t t2 H0) in
55 H_y))) in (let H2 \def (eq_ind_r T t2 (\lambda (t0: T).(pr2 (CHead c (Bind
56 Abst) u) t t0)) H0 t H1) in (eq_ind T t (\lambda (t0: T).(eq T t t0))
57 (refl_equal T t) t2 H1))))))))).
60 \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Flat Cast) u
61 t)) \to (\forall (P: Prop).P))))
63 \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (nf2 c (THead
64 (Flat Cast) u t))).(\lambda (P: Prop).(thead_x_y_y (Flat Cast) u t (H t
65 (pr2_free c (THead (Flat Cast) u t) t (pr0_epsilon t t (pr0_refl t) u)))
69 \forall (f: F).(\forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c
70 (THead (Flat f) u t)) \to (land (nf2 c u) (nf2 c t))))))
72 \lambda (f: F).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H:
73 ((\forall (t2: T).((pr2 c (THead (Flat f) u t) t2) \to (eq T (THead (Flat f)
74 u t) t2))))).(conj (\forall (t2: T).((pr2 c u t2) \to (eq T u t2))) (\forall
75 (t2: T).((pr2 c t t2) \to (eq T t t2))) (\lambda (t2: T).(\lambda (H0: (pr2 c
76 u t2)).(let H1 \def (f_equal T T (\lambda (e: T).(match e in T return
77 (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u |
78 (THead _ t0 _) \Rightarrow t0])) (THead (Flat f) u t) (THead (Flat f) t2 t)
79 (H (THead (Flat f) t2 t) (pr2_head_1 c u t2 H0 (Flat f) t))) in H1)))
80 (\lambda (t2: T).(\lambda (H0: (pr2 c t t2)).(let H1 \def (f_equal T T
81 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
82 \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t0) \Rightarrow t0]))
83 (THead (Flat f) u t) (THead (Flat f) u t2) (H (THead (Flat f) u t2)
84 (pr2_head_2 c u t t2 (Flat f) (pr2_cflat c t t2 H0 f u)))) in H1)))))))).