]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_1A/T/fwd.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / basic_1A / T / fwd.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/defs.ma".
18
19 implied rec lemma T_rect (P: (T \to Type[0])) (f: (\forall (n: nat).(P (TSort 
20 n)))) (f0: (\forall (n: nat).(P (TLRef n)))) (f1: (\forall (k: K).(\forall 
21 (t: T).((P t) \to (\forall (t0: T).((P t0) \to (P (THead k t t0)))))))) (t: 
22 T) on t: P t \def match t with [(TSort n) \Rightarrow (f n) | (TLRef n) 
23 \Rightarrow (f0 n) | (THead k t0 t1) \Rightarrow (f1 k t0 ((T_rect P f f0 f1) 
24 t0) t1 ((T_rect P f f0 f1) t1))].
25
26 implied lemma T_ind:
27  \forall (P: ((T \to Prop))).(((\forall (n: nat).(P (TSort n)))) \to 
28 (((\forall (n: nat).(P (TLRef n)))) \to (((\forall (k: K).(\forall (t: T).((P 
29 t) \to (\forall (t0: T).((P t0) \to (P (THead k t t0)))))))) \to (\forall (t: 
30 T).(P t)))))
31 \def
32  \lambda (P: ((T \to Prop))).(T_rect P).
33
34 lemma thead_x_y_y:
35  \forall (k: K).(\forall (v: T).(\forall (t: T).((eq T (THead k v t) t) \to 
36 (\forall (P: Prop).P))))
37 \def
38  \lambda (k: K).(\lambda (v: T).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq 
39 T (THead k v t0) t0) \to (\forall (P: Prop).P))) (\lambda (n: nat).(\lambda 
40 (H: (eq T (THead k v (TSort n)) (TSort n))).(\lambda (P: Prop).(let H0 \def 
41 (eq_ind T (THead k v (TSort n)) (\lambda (ee: T).(match ee with [(TSort _) 
42 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow 
43 True])) I (TSort n) H) in (False_ind P H0))))) (\lambda (n: nat).(\lambda (H: 
44 (eq T (THead k v (TLRef n)) (TLRef n))).(\lambda (P: Prop).(let H0 \def 
45 (eq_ind T (THead k v (TLRef n)) (\lambda (ee: T).(match ee with [(TSort _) 
46 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow 
47 True])) I (TLRef n) H) in (False_ind P H0))))) (\lambda (k0: K).(\lambda (t0: 
48 T).(\lambda (_: (((eq T (THead k v t0) t0) \to (\forall (P: 
49 Prop).P)))).(\lambda (t1: T).(\lambda (H0: (((eq T (THead k v t1) t1) \to 
50 (\forall (P: Prop).P)))).(\lambda (H1: (eq T (THead k v (THead k0 t0 t1)) 
51 (THead k0 t0 t1))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e: 
52 T).(match e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead 
53 k1 _ _) \Rightarrow k1])) (THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) 
54 in ((let H3 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
55 \Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t2 _) \Rightarrow t2])) 
56 (THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) in ((let H4 \def (f_equal T 
57 T (\lambda (e: T).(match e with [(TSort _) \Rightarrow (THead k0 t0 t1) | 
58 (TLRef _) \Rightarrow (THead k0 t0 t1) | (THead _ _ t2) \Rightarrow t2])) 
59 (THead k v (THead k0 t0 t1)) (THead k0 t0 t1) H1) in (\lambda (H5: (eq T v 
60 t0)).(\lambda (H6: (eq K k k0)).(let H7 \def (eq_ind T v (\lambda (t2: 
61 T).((eq T (THead k t2 t1) t1) \to (\forall (P0: Prop).P0))) H0 t0 H5) in (let 
62 H8 \def (eq_ind K k (\lambda (k1: K).((eq T (THead k1 t0 t1) t1) \to (\forall 
63 (P0: Prop).P0))) H7 k0 H6) in (H8 H4 P)))))) H3)) H2))))))))) t))).
64