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 "basic_1/T/defs.ma".
19 let rec T_rect (P: (T \to Type[0])) (f: (\forall (n: nat).(P (TSort n))))
20 (f0: (\forall (n: nat).(P (TLRef n)))) (f1: (\forall (k: K).(\forall (t:
21 T).((P t) \to (\forall (t0: T).((P t0) \to (P (THead k t t0)))))))) (t: T) on
22 t: P t \def match t with [(TSort n) \Rightarrow (f n) | (TLRef n) \Rightarrow
23 (f0 n) | (THead k t0 t1) \Rightarrow (let TMP_1 \def ((T_rect P f f0 f1) t0)
24 in (let TMP_2 \def ((T_rect P f f0 f1) t1) in (f1 k t0 TMP_1 t1 TMP_2)))].
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:
32 \lambda (P: ((T \to Prop))).(T_rect P).
35 \forall (k: K).(\forall (v: T).(\forall (t: T).((eq T (THead k v t) t) \to
36 (\forall (P: Prop).P))))
38 \lambda (k: K).(\lambda (v: T).(\lambda (t: T).(let TMP_1 \def (\lambda (t0:
39 T).((eq T (THead k v t0) t0) \to (\forall (P: Prop).P))) in (let TMP_6 \def
40 (\lambda (n: nat).(\lambda (H: (eq T (THead k v (TSort n)) (TSort
41 n))).(\lambda (P: Prop).(let TMP_2 \def (TSort n) in (let TMP_3 \def (THead k
42 v TMP_2) in (let TMP_4 \def (\lambda (ee: T).(match ee with [(TSort _)
43 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
44 True])) in (let TMP_5 \def (TSort n) in (let H0 \def (eq_ind T TMP_3 TMP_4 I
45 TMP_5 H) in (False_ind P H0))))))))) in (let TMP_11 \def (\lambda (n:
46 nat).(\lambda (H: (eq T (THead k v (TLRef n)) (TLRef n))).(\lambda (P:
47 Prop).(let TMP_7 \def (TLRef n) in (let TMP_8 \def (THead k v TMP_7) in (let
48 TMP_9 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
49 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) in (let
50 TMP_10 \def (TLRef n) in (let H0 \def (eq_ind T TMP_8 TMP_9 I TMP_10 H) in
51 (False_ind P H0))))))))) in (let TMP_28 \def (\lambda (k0: K).(\lambda (t0:
52 T).(\lambda (_: (((eq T (THead k v t0) t0) \to (\forall (P:
53 Prop).P)))).(\lambda (t1: T).(\lambda (H0: (((eq T (THead k v t1) t1) \to
54 (\forall (P: Prop).P)))).(\lambda (H1: (eq T (THead k v (THead k0 t0 t1))
55 (THead k0 t0 t1))).(\lambda (P: Prop).(let TMP_12 \def (\lambda (e: T).(match
56 e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k1 _ _)
57 \Rightarrow k1])) in (let TMP_13 \def (THead k0 t0 t1) in (let TMP_14 \def
58 (THead k v TMP_13) in (let TMP_15 \def (THead k0 t0 t1) in (let H2 \def
59 (f_equal T K TMP_12 TMP_14 TMP_15 H1) in (let TMP_16 \def (\lambda (e:
60 T).(match e with [(TSort _) \Rightarrow v | (TLRef _) \Rightarrow v | (THead
61 _ t2 _) \Rightarrow t2])) in (let TMP_17 \def (THead k0 t0 t1) in (let TMP_18
62 \def (THead k v TMP_17) in (let TMP_19 \def (THead k0 t0 t1) in (let H3 \def
63 (f_equal T T TMP_16 TMP_18 TMP_19 H1) in (let TMP_20 \def (\lambda (e:
64 T).(match e with [(TSort _) \Rightarrow (THead k0 t0 t1) | (TLRef _)
65 \Rightarrow (THead k0 t0 t1) | (THead _ _ t2) \Rightarrow t2])) in (let
66 TMP_21 \def (THead k0 t0 t1) in (let TMP_22 \def (THead k v TMP_21) in (let
67 TMP_23 \def (THead k0 t0 t1) in (let H4 \def (f_equal T T TMP_20 TMP_22
68 TMP_23 H1) in (let TMP_26 \def (\lambda (H5: (eq T v t0)).(\lambda (H6: (eq K
69 k k0)).(let TMP_24 \def (\lambda (t2: T).((eq T (THead k t2 t1) t1) \to
70 (\forall (P0: Prop).P0))) in (let H7 \def (eq_ind T v TMP_24 H0 t0 H5) in
71 (let TMP_25 \def (\lambda (k1: K).((eq T (THead k1 t0 t1) t1) \to (\forall
72 (P0: Prop).P0))) in (let H8 \def (eq_ind K k TMP_25 H7 k0 H6) in (H8 H4
73 P))))))) in (let TMP_27 \def (TMP_26 H3) in (TMP_27
74 H2))))))))))))))))))))))))) in (T_ind TMP_1 TMP_6 TMP_11 TMP_28 t))))))).