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 "LambdaDelta-1/nf2/pr3.ma".
19 include "LambdaDelta-1/pr3/fwd.ma".
21 include "LambdaDelta-1/iso/props.ma".
23 theorem nf2_iso_appls_lref:
24 \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs:
25 TList).(\forall (u: T).((pr3 c (THeads (Flat Appl) vs (TLRef i)) u) \to (iso
26 (THeads (Flat Appl) vs (TLRef i)) u))))))
28 \lambda (c: C).(\lambda (i: nat).(\lambda (H: (nf2 c (TLRef i))).(\lambda
29 (vs: TList).(TList_ind (\lambda (t: TList).(\forall (u: T).((pr3 c (THeads
30 (Flat Appl) t (TLRef i)) u) \to (iso (THeads (Flat Appl) t (TLRef i)) u))))
31 (\lambda (u: T).(\lambda (H0: (pr3 c (TLRef i) u)).(let H_y \def
32 (nf2_pr3_unfold c (TLRef i) u H0 H) in (let H1 \def (eq_ind_r T u (\lambda
33 (t: T).(pr3 c (TLRef i) t)) H0 (TLRef i) H_y) in (eq_ind T (TLRef i) (\lambda
34 (t: T).(iso (TLRef i) t)) (iso_refl (TLRef i)) u H_y))))) (\lambda (t:
35 T).(\lambda (t0: TList).(\lambda (H0: ((\forall (u: T).((pr3 c (THeads (Flat
36 Appl) t0 (TLRef i)) u) \to (iso (THeads (Flat Appl) t0 (TLRef i))
37 u))))).(\lambda (u: T).(\lambda (H1: (pr3 c (THead (Flat Appl) t (THeads
38 (Flat Appl) t0 (TLRef i))) u)).(let H2 \def (pr3_gen_appl c t (THeads (Flat
39 Appl) t0 (TLRef i)) u H1) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda
40 (t2: T).(eq T u (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
41 T).(pr3 c t u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c (THeads (Flat Appl)
42 t0 (TLRef i)) t2)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_: T).(\lambda
43 (u2: T).(\lambda (t2: T).(pr3 c (THead (Bind Abbr) u2 t2) u))))) (\lambda (_:
44 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))))) (\lambda
45 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(pr3 c (THeads (Flat
46 Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda
47 (z1: T).(\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u0:
48 T).(pr3 (CHead c (Bind b) u0) z1 t2)))))))) (ex6_6 B T T T T T (\lambda (b:
49 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
50 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
51 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c (THeads (Flat
52 Appl) t0 (TLRef i)) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda
53 (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2:
54 T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
55 u))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
56 T).(\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))))))) (\lambda (_:
57 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
58 (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
59 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b)
60 y2) z1 z2)))))))) (iso (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef
61 i))) u) (\lambda (H3: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T u
62 (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c t u2)))
63 (\lambda (_: T).(\lambda (t2: T).(pr3 c (THeads (Flat Appl) t0 (TLRef i))
64 t2))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t2: T).(eq T u (THead (Flat
65 Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))) (\lambda (_:
66 T).(\lambda (t2: T).(pr3 c (THeads (Flat Appl) t0 (TLRef i)) t2))) (iso
67 (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u) (\lambda (x0:
68 T).(\lambda (x1: T).(\lambda (H4: (eq T u (THead (Flat Appl) x0
69 x1))).(\lambda (_: (pr3 c t x0)).(\lambda (_: (pr3 c (THeads (Flat Appl) t0
70 (TLRef i)) x1)).(eq_ind_r T (THead (Flat Appl) x0 x1) (\lambda (t1: T).(iso
71 (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t1)) (iso_head t x0
72 (THeads (Flat Appl) t0 (TLRef i)) x1 (Flat Appl)) u H4)))))) H3)) (\lambda
73 (H3: (ex4_4 T T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
74 (t2: T).(pr3 c (THead (Bind Abbr) u2 t2) u))))) (\lambda (_: T).(\lambda (_:
75 T).(\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))))) (\lambda (y1:
76 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(pr3 c (THeads (Flat
77 Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda
78 (z1: T).(\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u0:
79 T).(pr3 (CHead c (Bind b) u0) z1 t2))))))))).(ex4_4_ind T T T T (\lambda (_:
80 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(pr3 c (THead (Bind
81 Abbr) u2 t2) u))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
82 (_: T).(pr3 c t u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
83 T).(\lambda (_: T).(pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind
84 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
85 (t2: T).(\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b) u0) z1
86 t2))))))) (iso (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u)
87 (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda
88 (_: (pr3 c (THead (Bind Abbr) x2 x3) u)).(\lambda (_: (pr3 c t x2)).(\lambda
89 (H6: (pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) x0
90 x1))).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b)
91 u0) x1 x3))))).(let H_y \def (H0 (THead (Bind Abst) x0 x1) H6) in
92 (iso_flats_lref_bind_false Appl Abst i x0 x1 t0 H_y (iso (THead (Flat Appl) t
93 (THeads (Flat Appl) t0 (TLRef i))) u))))))))))) H3)) (\lambda (H3: (ex6_6 B T
94 T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
95 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
96 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
97 (_: T).(pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind b) y1 z1))))))))
98 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda
99 (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift
100 (S O) O u2) z2)) u))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
101 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c t u2)))))))
102 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
103 T).(\lambda (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_:
104 T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3
105 (CHead c (Bind b) y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b:
106 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
107 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
108 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c (THeads (Flat
109 Appl) t0 (TLRef i)) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda
110 (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2:
111 T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
112 u))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
113 T).(\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))))))) (\lambda (_:
114 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
115 (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
116 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b)
117 y2) z1 z2))))))) (iso (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i)))
118 u) (\lambda (x0: B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
119 T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (not (eq B x0
120 Abst))).(\lambda (H5: (pr3 c (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind
121 x0) x1 x2))).(\lambda (_: (pr3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift
122 (S O) O x4) x3)) u)).(\lambda (_: (pr3 c t x4)).(\lambda (_: (pr3 c x1
123 x5)).(\lambda (_: (pr3 (CHead c (Bind x0) x5) x2 x3)).(let H_y \def (H0
124 (THead (Bind x0) x1 x2) H5) in (iso_flats_lref_bind_false Appl x0 i x1 x2 t0
125 H_y (iso (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i)))
126 u))))))))))))))) H3)) H2))))))) vs)))).