2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "lambda/subterms.ma".
15 inductive T : Type[0] ≝
19 | Lambda: T → T → T (* type, body *)
20 | Prod: T → T → T (* type, body *)
36 theorem is_dummy_to_exists: ∀M. is_dummy M = true →
38 #M (cases M) normalize
39 [1,2: #n #H destruct|3,4,5: #P #Q #H destruct
40 |#N #_ @(ex_intro … N) //
44 theorem is_lambda_to_exists: ∀M. is_lambda M = true →
46 #M (cases M) normalize
47 [1,2,6: #n #H destruct|3,5: #P #Q #H destruct
48 |#P #N #_ @(ex_intro … P) @(ex_intro … N) //
52 inductive pr : T →T → Prop ≝
53 | beta: ∀P,M,N,M1,N1. pr M M1 → pr N N1 →
54 pr (App (Lambda P M) N) (M1[0 ≝ N1])
55 | dapp: ∀M,N,P. pr (App M N) P →
56 pr (App (D M) N) (D P)
57 | dlam: ∀M,N,P. pr (Lambda M N) P → pr (Lambda M (D N)) (D P)
59 | appl: ∀M,M1,N,N1. pr M M1 → pr N N1 → pr (App M N) (App M1 N1)
60 | lam: ∀P,P1,M,M1. pr P P1 → pr M M1 →
61 pr (Lambda P M) (Lambda P1 M1)
62 | prod: ∀P,P1,M,M1. pr P P1 → pr M M1 →
63 pr (Prod P M) (Prod P1 M1)
64 | d: ∀M,M1. pr M M1 → pr (D M) (D M1).
66 lemma prSort: ∀M,n. pr (Sort n) M → M = Sort n.
67 #M #n #prH (inversion prH)
68 [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
69 |#M #N #P1 #_ #_ #H destruct
70 |#M #N #P1 #_ #_ #H destruct
72 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
73 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
74 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
75 |#M #N #_ #_ #H destruct
79 lemma prRel: ∀M,n. pr (Rel n) M → M = Rel n.
80 #M #n #prH (inversion prH)
81 [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
82 |#M #N #P1 #_ #_ #H destruct
83 |#M #N #P1 #_ #_ #H destruct
85 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
86 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
87 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
88 |#M #N #_ #_ #H destruct
92 lemma prD: ∀M,N. pr (D N) M → ∃P.M = D P ∧ pr N P.
93 #M #N #prH (inversion prH)
94 [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
95 |#M #N #P #_ #_ #H destruct
96 |#M #N #P1 #_ #_ #H destruct
97 |#R #eqR <eqR #_ @(ex_intro … N) /2/
98 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
99 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
100 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
101 |#M1 #N1 #pr #_ #H destruct #eqM @(ex_intro … N1) /2/
105 lemma prApp_not_dummy_not_lambda:
106 ∀M,N,P. pr (App M N) P → is_dummy M = false → is_lambda M = false →
107 ∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
108 #M #N #P #prH (inversion prH)
109 [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #_ #H1 destruct
110 |#M1 #N1 #P1 #_ #_ #H destruct #_ #H1 destruct
111 |#M #N #P1 #_ #_ #H destruct
112 |#Q #eqProd #_ #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
113 |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H #H1 #_ #_ destruct
114 @(ex_intro … N1) @(ex_intro … N2) /3/
115 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
116 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
117 |#M #N #_ #_ #H destruct
122 ∀M,N,P. pr (App (D M) N) P →
123 (∃Q. (P = D Q ∧ pr (App M N) Q)) ∨
124 (∃M1,N1.(P = (App (D M1) N1) ∧ pr M M1 ∧ pr N N1)).
125 #M #N #P #prH (inversion prH)
126 [#R #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
127 |#M1 #N1 #P1 #pr1 #_ #H destruct #eqP
128 @or_introl @(ex_intro … P1) /2/
129 |#M #N #P1 #_ #_ #H destruct
130 |#R #eqR #_ @or_intror @(ex_intro … M) @(ex_intro … N) /3/
131 |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
132 cases (prD … pr1) #S * #eqN1 >eqN1 #pr3
133 @or_intror @(ex_intro … S) @(ex_intro … N2) /3/
134 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
135 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
136 |#M #N #_ #_ #H destruct
141 ∀Q,M,N,P. pr (App (Lambda Q M) N) P →
142 ∃M1,N1. (P = M1[0:=N1] ∧ pr M M1 ∧ pr N N1) ∨
143 (P = (App M1 N1) ∧ pr (Lambda Q M) M1 ∧ pr N N1).
144 #Q #M #N #P #prH (inversion prH)
145 [#R #M #N #M1 #N1 #pr1 #pr2 #_ #_ #H destruct #_
146 @(ex_intro … M1) @(ex_intro … N1) /4/
147 |#M1 #N1 #P1 #_ #_ #H destruct
148 |#M #N #P1 #_ #_ #H destruct
149 |#R #eqR #_ @(ex_intro … (Lambda Q M)) @(ex_intro … N) /4/
150 |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
151 @(ex_intro … N1) @(ex_intro … N2) /4/
152 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
153 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
154 |#M #N #_ #_ #H destruct
158 lemma prLambda_not_dummy: ∀M,N,P. pr (Lambda M N) P → is_dummy N = false →
159 ∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1).
160 #M #N #P #prH (inversion prH)
161 [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
162 |#M #N #P1 #_ #_ #H destruct
163 |#M #N #P1 #_ #_ #H destruct #_ #eqH destruct
164 |#Q #eqProd #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
165 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
166 |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 #_ destruct
167 @(ex_intro … Q1) @(ex_intro … S1) /3/
168 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
169 |#M #N #_ #_ #H destruct
173 lemma prLambda_dummy: ∀M,N,P. pr (Lambda M (D N)) P →
174 (∃M1,N1. P = Lambda M1 (D N1) ∧ pr M M1 ∧ pr N N1) ∨
175 (∃Q. (P = D Q ∧ pr (Lambda M N) Q)).
176 #M #N #P #prH (inversion prH)
177 [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
178 |#M #N #P1 #_ #_ #H destruct
179 |#M1 #N1 #P1 #prM #_ #eqlam destruct #H @or_intror
181 |#Q #eqLam #_ @or_introl @(ex_intro … M) @(ex_intro … N) /3/
182 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
183 |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
184 cases (prD …pr2) #S2 * #eqS1 #pr3 >eqS1 @or_introl
185 @(ex_intro … Q1) @(ex_intro … S2) /3/
186 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
187 |#M #N #_ #_ #H destruct
191 lemma prLambda: ∀M,N,P. pr (Lambda M N) P →
192 (∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1)) ∨
193 (∃N1,Q. (N=D N1) ∧ (P = (D Q) ∧ pr (Lambda M N1) Q)).
194 #M #N #P #prH (inversion prH)
195 [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
196 |#M #N #P1 #_ #_ #H destruct
197 |#M1 #N1 #P1 #prM1 #_ #eqlam #eqP destruct @or_intror
198 @(ex_intro … N1) @(ex_intro … P1) /3/
199 |#Q #eqProd #_ @or_introl @(ex_intro … M) @(ex_intro … N) /3/
200 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
201 |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct @or_introl
202 @(ex_intro … Q1) @(ex_intro … S1) /3/
203 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
204 |#M #N #_ #_ #H destruct
208 lemma prProd: ∀M,N,P. pr (Prod M N) P →
209 ∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1.
210 #M #N #P #prH (inversion prH)
211 [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
212 |#M #N #P1 #_ #_ #H destruct
213 |#M #N #P1 #_ #_ #H destruct
214 |#Q #eqProd #_ @(ex_intro … M) @(ex_intro … N) /3/
215 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
216 |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
217 |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
218 @(ex_intro … Q1) @(ex_intro … S1) /3/
219 |#M #N #_ #_ #H destruct
227 | App P Q ⇒ full_app P (full Q)
228 | Lambda P Q ⇒ full_lam (full P) Q
229 | Prod P Q ⇒ Prod (full P) (full Q)
234 [ Sort n ⇒ App (Sort n) N
235 | Rel n ⇒ App (Rel n) N
236 | App P Q ⇒ App (full_app P (full Q)) N
237 | Lambda P Q ⇒ (full Q) [0 ≝ N]
238 | Prod P Q ⇒ App (Prod (full P) (full Q)) N
239 | D P ⇒ D (full_app P N)
241 and full_lam M N on N≝
243 [ Sort n ⇒ Lambda M (Sort n)
244 | Rel n ⇒ Lambda M (Rel n)
245 | App P Q ⇒ Lambda M (full_app P (full Q))
246 | Lambda P Q ⇒ Lambda M (full_lam (full P) Q)
247 | Prod P Q ⇒ Lambda M (Prod (full P) (full Q))
248 | D P ⇒ D (full_lam M P)
252 lemma pr_lift: ∀N,N1,n. pr N N1 → ∀k. pr (lift N k n) (lift N1 k n).
253 #N #N1 #n #pr1 (elim pr1)
254 [#P #M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
255 normalize >lift_subst_up @beta; //
256 |#M1 #N1 #P #pr2 #Hind normalize #k @dapp @Hind
257 |#M1 #N1 #P #pr2 #Hind normalize #k @dlam @Hind
259 |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
260 normalize @appl; [@Hind1 |@Hind2]
261 |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
262 normalize @lam; [@Hind1 |@Hind2]
263 |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
264 normalize @prod; [@Hind1 |@Hind2]
265 |#M1 #M2 #pr2 #Hind #k normalize @d //
269 theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 →
271 @Telim_size #P (cases P)
272 [#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prSort … pr1) //
273 |#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prRel … pr1)
274 (cases (true_or_false (leb i n)))
275 [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein)))
276 [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) //
277 |#eqin >eqin >subst_rel2 >subst_rel2 /2/
279 |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
280 >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
282 |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
283 (cases (true_or_false (is_dummy Q)))
284 [#isdummy (cases (is_dummy_to_exists … isdummy))
285 #Q1 #eqM >eqM in pr1 #pr3 (cases (prApp_D … pr3))
286 [* #Q2 * #eqM1 #pr4 >eqM1 @dapp @(Hind (App Q1 M)) //
288 |* #M2 * #N2 * * #eqM1 #pr4 #pr5 >eqM1 @appl;
289 [@Hind // [<eqM normalize // | @d //]
290 |@Hind // normalize //
294 (cases (true_or_false (is_lambda Q)))
295 [#islambda (cases (is_lambda_to_exists … islambda))
296 #M2 * #N2 #eqQ >eqQ in pr1 #pr3 (cases (prApp_lambda … pr3))
298 [* * #eqM1 #pr4 #pr5 >eqM1
299 >(plus_n_O n) in ⊢ (??%) >subst_lemma
301 [<plus_n_Sm <plus_n_O @Hind // >eqQ
302 @(transitive_lt ? (size (Lambda M2 N2))) normalize //
303 |@Hind // normalize //
305 |* * #eqM1 #pr4 #pr5 >eqM1 @appl;
306 [@Hind // <eqQ normalize //
307 |@Hind // normalize //
310 |#notlambda (cases (prApp_not_dummy_not_lambda … pr1 ??)) //
311 #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @appl;
312 [@Hind // normalize // |@Hind // normalize // ]
315 |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
316 (cases (prLambda … pr1))
317 [* #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @lam;
318 [@Hind // normalize // | @Hind // normalize // ]
319 |* #N2 * #Q1 * #eqM * #eqM1 #pr3 >eqM >eqM1 @dlam
320 @(Hind (Lambda Q N2)) // >eqM normalize //
322 |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
323 (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1
324 @prod; [@Hind // normalize // | @Hind // normalize // ]
325 |#Q #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prD … pr1))
326 #M2 * #eqM1 #pr1 >eqM1 @d @Hind // normalize //
330 lemma pr_full_app: ∀M,N,N1. pr N N1 →
331 (∀S.subterm S M → pr S (full S)) →
332 pr (App M N) (full_app M N1).
333 #M (elim M) normalize /2/
334 [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @Hind1 /3/
335 |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @beta /2/
336 |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @prod /2/
337 |#P #Hind #N1 #N2 #prN #H @dapp @Hind /3/
341 lemma pr_full_lam: ∀M,N,N1. pr N N1 →
342 (∀S.subterm S M → pr S (full S)) →
343 pr (Lambda N M) (full_lam N1 M).
344 #M (elim M) normalize /2/
345 [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @pr_full_app /3/
346 |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @Hind2 /3/
347 |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @lam // @prod /2/
348 |#P #Hind #N1 #N2 #prN #H @dlam @Hind /3/
352 theorem pr_full: ∀M. pr M (full M).
356 |#M1 #N1 #H @pr_full_app /3/
357 |#M1 #N1 #H @pr_full_lam /3/
358 |#M1 #N1 #H @prod /2/
363 lemma complete_beta: ∀Q,N,N1,M,M1.(* pr N N1 → *) pr N1 (full N) →
364 (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
365 pr (Lambda Q M) M1 → pr (App M1 N1) ((full M) [O ≝ (full N)]).
366 #Q #N #N1 #M (elim M)
367 [1,2:#n #M1 #prN1 #sub #pr1
368 (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
369 * * #eqM1 #pr3 #pr4 >eqM1 @beta /3/
370 |3,4,5:#M1 #M2 #_ #_ #M3 #prN1 #sub #pr1
371 (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
372 * * #eqM3 #pr3 #pr4 >eqM3 @beta /3/
373 |#M1 #Hind #M2 #prN1 #sub #pr1
374 (cases (prLambda_dummy … pr1))
375 [* #M3 * #N3 * * #eqM2 #pr3 #pr4 >eqM2
376 @beta // normalize @d @sub /2/
377 |* #P * #eqM2 #pr3 >eqM2 normalize @dapp
378 @Hind // #S #P #subH #pr4 @sub //
379 (cases (sublam … subH)) [* [* /2/ | /2/] | /3/
384 lemma complete_beta1: ∀Q,N,M,M1.
385 (∀N1. pr N N1 → pr N1 (full N)) →
386 (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
387 pr (App (Lambda Q M) N) M1 → pr M1 ((full M) [O ≝ (full N)]).
388 #Q #N #M #M1 #prH #subH #prApp
389 (cases (prApp_lambda … prApp)) #M2 * #N2 *
390 [* * #eqM1 #pr1 #pr2 >eqM1 @pr_subst; [@subH // | @prH //]
391 |* * #eqM1 #pr1 #pr2 >eqM1 @(complete_beta … pr1);
393 |#S #P #subS #prS @subH //
398 lemma complete_app: ∀M,N,P.
399 (∀S,P.subterm S (App M N) → pr S P → pr P (full S)) →
400 pr (App M N) P → pr P (full_app M (full N)).
401 #M (elim M) normalize
403 cases (prApp_not_dummy_not_lambda … pr1 ??) //
404 #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
405 [@(Hind (Sort n)) // |@Hind //]
407 cases (prApp_not_dummy_not_lambda … pr1 ??) //
408 #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl;
409 [@(Hind (Rel n)) // |@Hind //]
410 |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
411 cases (prApp_not_dummy_not_lambda … prH ??) //
412 #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
413 [@Hind1 /3/ |@subH //]
414 |#P #Q #Hind1 #Hind2 #N1 #P2 #subH #prH
415 @(complete_beta1 … prH);
416 [#N2 @subH // | #S #P1 #subS @subH
417 (cases (sublam … subS)) [* [* /2/ | /2/] | /2/]
419 |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
420 cases (prApp_not_dummy_not_lambda … prH ??) //
421 #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl;
422 [@(subH (Prod P Q)) // |@subH //]
423 |#P #Hind #N1 #N2 #subH #prH
424 (cut (∀S. subterm S (App P N1) → subterm S (App (D P) N1)))
425 [#S #sub (cases (subapp …sub)) [* [ * /2/ | /3/] | /2/]] #Hcut
426 cases (prApp_D … prH);
427 [* #N3 * #eqN3 #pr1 >eqN3 @d @Hind //
428 #S #P1 #sub1 #prS @subH /2/
429 |* #N3 * #N4 * * #eqN2 #prP #prN1 >eqN2 @dapp @Hind;
430 [#S #P1 #sub1 #prS @subH /2/ |@appl // ]
435 lemma complete_lam: ∀M,Q,M1.
436 (∀S,P.subterm S (Lambda Q M) → pr S P → pr P (full S)) →
437 pr (Lambda Q M) M1 → pr M1 (full_lam (full Q) M).
439 [#n #Q #M1 #sub #pr1 normalize
440 (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
441 * * #eqM1 #pr3 #pr4 >eqM1 @lam;
442 [@sub /2/ | @(sub (Sort n)) /2/]
443 |#n #Q #M1 #sub #pr1 normalize
444 (cases (prLambda_not_dummy … pr1 ?)) // #M2 * #N2
445 * * #eqM1 #pr3 #pr4 >eqM1 @lam;
446 [@sub /2/ | @(sub (Rel n)) /2/]
447 |#M1 #M2 #_ #_ #M3 #Q #sub #pr1
448 (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
449 * * #eqM3 #pr3 #pr4 >eqM3 @lam;
450 [@sub // | @complete_app // #S #P1 #subS @sub
451 (cases (subapp …subS)) [* [* /2/ | /2/] | /3/ ]
453 |#M1 #M2 #_ #Hind #M3 #Q #sub #pr1
454 (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
455 * * #eqM3 #pr3 #pr4 >eqM3 @lam;
456 [@sub // |@Hind // #S #P1 #subS @sub
457 (cases (sublam …subS)) [* [* /2/ | /2/] | /3/ ]
459 |#M1 #M2 #_ #_ #M3 #Q #sub #pr1
460 (cases (prLambda_not_dummy … pr1 ?)) // #M4 * #N3
461 * * #eqM3 #pr3 #pr4 >eqM3 @lam;
462 [@sub // | (cases (prProd … pr4)) #M5 * #N4 * * #eqN3
463 #pr5 #pr6 >eqN3 @prod;
464 [@sub /3/ | @sub /3/]
466 |#P #Hind #Q #M2 #sub #pr1 (cases (prLambda_dummy … pr1))
467 [* #M3 * #N3 * * #eqM2 #pr3 #pr4 >eqM2 normalize
469 [#S #P1 #subS @sub (cases (sublam …subS))
470 [* [* /2/ | /2/ ] |/3/ ]
473 |* #P * #eqM2 #pr3 >eqM2 normalize @d
474 @Hind // #S #P #subH @sub
475 (cases (sublam … subH)) [* [* /2/ | /2/] | /3/]
480 theorem complete: ∀M,N. pr M N → pr N (full M).
482 [#n #Hind #N #prH normalize >(prSort … prH) //
483 |#n #Hind #N #prH normalize >(prRel … prH) //
484 |#M #N #Hind #Q @complete_app
486 | #P #P1 #Hind #N #Hpr @(complete_lam … Hpr)
488 |5: #P #P1 #Hind #N #Hpr
489 (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
490 |6:#N #Hind #P #prH normalize cases (prD … prH)
491 #Q * #eqP >eqP #prN @d @Hind //
495 theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S.
497 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/