1 (* (C) 2014 Luca Bressan *)
6 definition proj1: ∀C: est. ∀r: list (Σx. Σy. x ≃ y). list C ≝
7 λC. lift_to_list … (π1 …).
9 definition proj2: ∀C: est. ∀r: list (Σx. Σy. x ≃ y). list C ≝
10 λC. lift_to_list … (λz: Σx. Σy. x ≃ y. π1 (π2 z)).
12 definition elist: est → est ≝
15 (λz,z'. ∃l: list (Σx. Σy. x ≃ y). (proj1 … l = z) ∧ (proj2 … l = z'))
19 | #l #c * #r * #h1 #h2
21 % [ @(rewrite_l … ⌈proj1 … r, c⌉
23 (rewrite_l … (proj1 … r) (λz. ⌈proj1 … r, c⌉ = ⌈z, c⌉) (reflexivity …) … h1)
25 | @(rewrite_l … ⌈proj2 … r, c⌉
27 (rewrite_l … (proj2 … r) (λz. ⌈proj2 … r, c⌉ = ⌈z, c⌉) (reflexivity …) … h2)
35 [ * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs))
36 | #r #s * normalize #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
41 [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
42 | #r #s * #_ normalize #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
45 [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
47 cut (∃l. (proj1 … l = l2') ∧ (proj2 … l = l1'))
48 [ @(h l2') %{r} % [ @(injectivity_cons1 … h1) | @(injectivity_cons1 … h2) ]
49 | * #r' * #h1' #h2' %{⌈r', 〈c2, 〈c1, ?〉〉⌉}
50 [ cut (π1 (π2 s) = c2)
51 [ cut (⌈proj2 … r, π1 (π2 s)⌉ = ⌈l2', c2⌉)
52 [ @(rewrite_l … (proj2 … ⌈r, s⌉)
53 (λz. z = ⌈l2', c2⌉) h2 … (reflexivity …))
57 [ cut (⌈proj1 … r, sig1 … s⌉ = ⌈l1', c1⌉)
58 [ @(rewrite_l … (proj1 … ⌈r, s⌉)
59 (λz. z = ⌈l1', c1⌉) h1 … (reflexivity …))
62 | #k1 cut (π1 (π2 s) ≃ π1 s)
65 [ @(rewrite_l … (π1 (π2 s)) (λz. z ≃ π1 s) e … k2)
66 | #e' @(rewrite_l … (π1 s) (λz. c2 ≃ z) e' … k1)
72 % [ @(rewrite_l … (proj1 … r') (λz. ⌈proj1 … r', c2⌉ = ⌈z, c2⌉) (reflexivity …) … h1')
73 | @(rewrite_l … (proj2 … r') (λz. ⌈proj2 … r', c1⌉ = ⌈z, c1⌉) (reflexivity …) … h2')
89 [ * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs))
90 | #r1' #s1 * #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
97 [ 1,3: * #abs @(falsum_rect_CProp0 … (list_clash … abs))
98 | 2,4: #r' #s * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
102 [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
103 | #r' #s * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
106 [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
107 | #r1 #s1 * #h1 #h2 * *
108 [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
110 cut (⌈proj1 … r1, π1 s1⌉ = ⌈l1', c1⌉)
111 [ @(rewrite_l … (proj1 … ⌈r1, s1⌉)
112 (λz. z = ⌈l1', c1⌉) h1 … (reflexivity …))
114 cut (⌈proj2 … r1, π1 (π2 s1)⌉ = ⌈l2', c2⌉)
115 [ @(rewrite_l … (proj2 … ⌈r1, s1⌉)
116 (λz. z = ⌈l2', c2⌉) h2 … (reflexivity …))
118 cut (⌈proj1 … r2, π1 s2⌉ = ⌈l2', c2⌉)
119 [ @(rewrite_l … (proj1 … ⌈r2, s2⌉)
120 (λz. z = ⌈l2', c2⌉) h3 … (reflexivity …))
122 cut (⌈proj2 … r2, π1 (π2 s2)⌉ = ⌈l3', c3⌉)
123 [ @(rewrite_l … (proj2 … ⌈r2, s2⌉)
124 (λz. z = ⌈l3', c3⌉) h4 … (reflexivity …))
126 cut (∃l. (proj1 … l = l1') ∧ (proj2 … l = l3'))
128 [ %{r1} @(mk_conj … (injectivity_cons1 … h1) (injectivity_cons1 … h2))
129 | %{r2} @(mk_conj … (injectivity_cons1 … h3) (injectivity_cons1 … h4))
131 | * #r * #e1 #e2 %{⌈r, 〈c1, 〈c3, ?〉〉⌉}
133 (rewrite_l … (π1 s1) (λz. z ≃ c2)
134 (rewrite_l … (π1 (π2 s1)) (λz. π1 s1 ≃ z) (π2 (π2 s1))
135 … (injectivity_cons2 … h2))
136 … (injectivity_cons2 … h1))
137 (rewrite_l … (π1 (π2 s2)) (λz. c2 ≃ z)
138 (rewrite_l … (π1 s2) (λz. z ≃ π1 (π2 s2)) (π2 (π2 s2))
139 … (injectivity_cons2 … h3))
140 … (injectivity_cons2 … h4)))
142 [ @(rewrite_l … (proj1 … r) (λz. ⌈proj1 … r, c1⌉ = ⌈z, c1⌉) (reflexivity …) … e1)
143 | @(rewrite_l … (proj2 … r) (λz. ⌈proj2 … r, c3⌉ = ⌈z, c3⌉) (reflexivity …) … e2)
159 definition eepsilon: ∀C: est. elist C ≝ epsilon.
161 definition econs: ∀C: est. eto (elist C) (eto C (elist C)) ≝
162 λC. 〈λl. 〈cons … l, ?〉, ?〉.
164 cut (subst C (constant_edst C (elist C)) c1 c2 d ⌈l, c1⌉ = ⌈l, c1⌉)
166 | #h @(rewrite_l (list (sup C)) ⌈l, c1⌉ (λz. eq (elist C) z ⌈l, c2⌉) ?
167 (subst C (constant_edst C (elist C)) c1 c2 d ⌈l, c1⌉) h)
168 @(list_rect_CProp0 … l)
169 [ %{⌈ϵ, 〈c1, 〈c2, d〉〉⌉} % %
171 [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
172 | #r' #s * #h1 #h2 %{⌈⌈r', 〈c, 〈c, ıc〉〉⌉, 〈c1, 〈c2, d〉〉⌉} %
173 [ change with (⌈⌈proj1 … , ?⌉, ?⌉) in ⊢ (??%?);
174 cut (proj1 … r' = l')
175 [ @(injectivity_cons1 … h1)
176 | #h @(rewrite_l ????? h) @reflexivity
178 | @(rewrite_l … ⌈⌈proj2 … r', c⌉, c2⌉ (λz. z = ⌈⌈l', c⌉, c2⌉) ?
179 (proj2 … ⌈⌈r', 〈c, 〈c, ıc〉〉⌉, 〈c1, 〈c2, d〉〉⌉) (reflexivity …))
180 cut (proj2 … r' = l')
181 [ @(injectivity_cons1 …
182 (rewrite_l … (proj2 … ⌈r', s⌉) (λz. ⌈proj2 … r', sig1 … (sig2 … s)⌉ = z)
183 (reflexivity …) ⌈l', c2⌉ h2))
184 | #h @(rewrite_l … l' (λz. ⌈⌈z, c⌉, c2⌉ = ⌈⌈l', c⌉, c2⌉) (reflexivity …)
185 (proj2 C r') (symmetry … h))
191 | #l1 #l2 * #r * #h1 #h2 #c %{⌈r, 〈c, 〈c, ıc〉〉⌉} %
192 [ @(rewrite_l … l1 (λz. ⌈z, c⌉ = ⌈l1, c⌉) (reflexivity …) (proj1 … r) (symmetry … h1))
193 | @(rewrite_l … l2 (λz. ⌈z, c⌉ = ⌈l2, c⌉) (reflexivity …) (proj2 … r) (symmetry … h2))