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/Level-1/LambdaDelta/pr2/subst1".
19 include "pr2/defs.ma".
21 include "pr0/subst1.ma".
23 include "csubst1/defs.ma".
25 include "subst1/subst1.ma".
27 include "getl/props.ma".
30 \forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
31 (CHead d (Bind Abbr) u)) \to (\forall (t1: T).(\forall (t2: T).((pr0 t1 t2)
32 \to (\forall (t: T).((subst1 i u t2 t) \to (pr2 c t1 t))))))))))
34 \lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
35 (H: (getl i c (CHead d (Bind Abbr) u))).(\lambda (t1: T).(\lambda (t2:
36 T).(\lambda (H0: (pr0 t1 t2)).(\lambda (t: T).(\lambda (H1: (subst1 i u t2
37 t)).(subst1_ind i u t2 (\lambda (t0: T).(pr2 c t1 t0)) (pr2_free c t1 t2 H0)
38 (\lambda (t0: T).(\lambda (H2: (subst0 i u t2 t0)).(pr2_delta c d u i H t1 t2
39 H0 t0 H2))) t H1)))))))))).
42 \forall (c: C).(\forall (e: C).(\forall (v: T).(\forall (i: nat).((getl i c
43 (CHead e (Bind Abbr) v)) \to (\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2)
44 \to (\forall (w1: T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c
45 w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))))))))))))
47 \lambda (c: C).(\lambda (e: C).(\lambda (v: T).(\lambda (i: nat).(\lambda
48 (H: (getl i c (CHead e (Bind Abbr) v))).(\lambda (t1: T).(\lambda (t2:
49 T).(\lambda (H0: (pr2 c t1 t2)).(let H1 \def (match H0 in pr2 return (\lambda
50 (c0: C).(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (pr2 c0 t t0)).((eq C
51 c0 c) \to ((eq T t t1) \to ((eq T t0 t2) \to (\forall (w1: T).((subst1 i v t1
52 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v
53 t2 w2)))))))))))) with [(pr2_free c0 t0 t3 H1) \Rightarrow (\lambda (H2: (eq
54 C c0 c)).(\lambda (H3: (eq T t0 t1)).(\lambda (H4: (eq T t3 t2)).(eq_ind C c
55 (\lambda (_: C).((eq T t0 t1) \to ((eq T t3 t2) \to ((pr0 t0 t3) \to (\forall
56 (w1: T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2))
57 (\lambda (w2: T).(subst1 i v t2 w2))))))))) (\lambda (H5: (eq T t0
58 t1)).(eq_ind T t1 (\lambda (t: T).((eq T t3 t2) \to ((pr0 t t3) \to (\forall
59 (w1: T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2))
60 (\lambda (w2: T).(subst1 i v t2 w2)))))))) (\lambda (H6: (eq T t3
61 t2)).(eq_ind T t2 (\lambda (t: T).((pr0 t1 t) \to (\forall (w1: T).((subst1 i
62 v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1
63 i v t2 w2))))))) (\lambda (H7: (pr0 t1 t2)).(\lambda (w1: T).(\lambda (H8:
64 (subst1 i v t1 w1)).(ex2_ind T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2:
65 T).(subst1 i v t2 w2)) (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2:
66 T).(subst1 i v t2 w2))) (\lambda (x: T).(\lambda (H9: (pr0 w1 x)).(\lambda
67 (H10: (subst1 i v t2 x)).(ex_intro2 T (\lambda (w2: T).(pr2 c w1 w2))
68 (\lambda (w2: T).(subst1 i v t2 w2)) x (pr2_free c w1 x H9) H10))))
69 (pr0_subst1 t1 t2 H7 v w1 i H8 v (pr0_refl v)))))) t3 (sym_eq T t3 t2 H6)))
70 t0 (sym_eq T t0 t1 H5))) c0 (sym_eq C c0 c H2) H3 H4 H1)))) | (pr2_delta c0 d
71 u i0 H1 t0 t3 H2 t H3) \Rightarrow (\lambda (H4: (eq C c0 c)).(\lambda (H5:
72 (eq T t0 t1)).(\lambda (H6: (eq T t t2)).(eq_ind C c (\lambda (c1: C).((eq T
73 t0 t1) \to ((eq T t t2) \to ((getl i0 c1 (CHead d (Bind Abbr) u)) \to ((pr0
74 t0 t3) \to ((subst0 i0 u t3 t) \to (\forall (w1: T).((subst1 i v t1 w1) \to
75 (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2
76 w2))))))))))) (\lambda (H7: (eq T t0 t1)).(eq_ind T t1 (\lambda (t4: T).((eq
77 T t t2) \to ((getl i0 c (CHead d (Bind Abbr) u)) \to ((pr0 t4 t3) \to
78 ((subst0 i0 u t3 t) \to (\forall (w1: T).((subst1 i v t1 w1) \to (ex2 T
79 (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))))))))))
80 (\lambda (H8: (eq T t t2)).(eq_ind T t2 (\lambda (t4: T).((getl i0 c (CHead d
81 (Bind Abbr) u)) \to ((pr0 t1 t3) \to ((subst0 i0 u t3 t4) \to (\forall (w1:
82 T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda
83 (w2: T).(subst1 i v t2 w2))))))))) (\lambda (H9: (getl i0 c (CHead d (Bind
84 Abbr) u))).(\lambda (H10: (pr0 t1 t3)).(\lambda (H11: (subst0 i0 u t3
85 t2)).(\lambda (w1: T).(\lambda (H12: (subst1 i v t1 w1)).(ex2_ind T (\lambda
86 (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst1 i v t3 w2)) (ex2 T (\lambda
87 (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))) (\lambda (x:
88 T).(\lambda (H13: (pr0 w1 x)).(\lambda (H14: (subst1 i v t3 x)).(neq_eq_e i
89 i0 (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2
90 w2))) (\lambda (H15: (not (eq nat i i0))).(ex2_ind T (\lambda (t4: T).(subst1
91 i v t2 t4)) (\lambda (t4: T).(subst1 i0 u x t4)) (ex2 T (\lambda (w2: T).(pr2
92 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))) (\lambda (x0: T).(\lambda
93 (H16: (subst1 i v t2 x0)).(\lambda (H17: (subst1 i0 u x x0)).(ex_intro2 T
94 (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2)) x0
95 (pr2_delta1 c d u i0 H9 w1 x H13 x0 H17) H16)))) (subst1_confluence_neq t3 t2
96 u i0 (subst1_single i0 u t3 t2 H11) x v i H14 (sym_not_eq nat i i0 H15))))
97 (\lambda (H15: (eq nat i i0)).(let H16 \def (eq_ind_r nat i0 (\lambda (n:
98 nat).(subst0 n u t3 t2)) H11 i H15) in (let H17 \def (eq_ind_r nat i0
99 (\lambda (n: nat).(getl n c (CHead d (Bind Abbr) u))) H9 i H15) in (let H18
100 \def (eq_ind C (CHead e (Bind Abbr) v) (\lambda (c1: C).(getl i c c1)) H
101 (CHead d (Bind Abbr) u) (getl_mono c (CHead e (Bind Abbr) v) i H (CHead d
102 (Bind Abbr) u) H17)) in (let H19 \def (f_equal C C (\lambda (e0: C).(match e0
103 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow e | (CHead c1 _ _)
104 \Rightarrow c1])) (CHead e (Bind Abbr) v) (CHead d (Bind Abbr) u) (getl_mono
105 c (CHead e (Bind Abbr) v) i H (CHead d (Bind Abbr) u) H17)) in ((let H20 \def
106 (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with
107 [(CSort _) \Rightarrow v | (CHead _ _ t4) \Rightarrow t4])) (CHead e (Bind
108 Abbr) v) (CHead d (Bind Abbr) u) (getl_mono c (CHead e (Bind Abbr) v) i H
109 (CHead d (Bind Abbr) u) H17)) in (\lambda (H21: (eq C e d)).(let H22 \def
110 (eq_ind_r T u (\lambda (t4: T).(getl i c (CHead d (Bind Abbr) t4))) H18 v
111 H20) in (let H23 \def (eq_ind_r T u (\lambda (t4: T).(subst0 i t4 t3 t2)) H16
112 v H20) in (let H24 \def (eq_ind_r C d (\lambda (c1: C).(getl i c (CHead c1
113 (Bind Abbr) v))) H22 e H21) in (ex2_ind T (\lambda (t4: T).(subst1 i v t2
114 t4)) (\lambda (t4: T).(subst1 i v x t4)) (ex2 T (\lambda (w2: T).(pr2 c w1
115 w2)) (\lambda (w2: T).(subst1 i v t2 w2))) (\lambda (x0: T).(\lambda (H25:
116 (subst1 i v t2 x0)).(\lambda (H26: (subst1 i v x x0)).(ex_intro2 T (\lambda
117 (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2)) x0 (pr2_delta1 c
118 e v i H24 w1 x H13 x0 H26) H25)))) (subst1_confluence_eq t3 t2 v i
119 (subst1_single i v t3 t2 H23) x H14))))))) H19)))))))))) (pr0_subst1 t1 t3
120 H10 v w1 i H12 v (pr0_refl v)))))))) t (sym_eq T t t2 H8))) t0 (sym_eq T t0
121 t1 H7))) c0 (sym_eq C c0 c H4) H5 H6 H1 H2 H3))))]) in (H1 (refl_equal C c)
122 (refl_equal T t1) (refl_equal T t2)))))))))).
125 \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
126 (e: C).(\forall (u: T).(\forall (d: nat).((getl d c (CHead e (Bind Abbr) u))
127 \to (\forall (a0: C).((csubst1 d u c a0) \to (\forall (a: C).((drop (S O) d
128 a0 a) \to (\forall (x1: T).((subst1 d u t1 (lift (S O) d x1)) \to (ex2 T
129 (\lambda (x2: T).(subst1 d u t2 (lift (S O) d x2))) (\lambda (x2: T).(pr2 a
130 x1 x2))))))))))))))))