+(*#* #stop file *)
+
Require pr0_confluence.
Require pr1_defs.
Theorem pr1_strip : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr0 t0 t2) ->
(EX t | (pr1 t1 t) & (pr1 t2 t)).
-
-(*#* #stop proof *)
-
Intros until 1; XElim H; Intros.
(* case 1 : pr1_r *)
XEAuto.
XElim H1; Intros; XEAuto.
Qed.
-(*#* #start proof *)
-
(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap t0, t1, t2, t *)
Theorem pr1_confluence : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr1 t0 t2) ->
(EX t | (pr1 t1 t) & (pr1 t2 t)).
-
-(*#* #stop file *)
-
Intros until 1; XElim H; Intros.
(* case 1 : pr1_r *)
XEAuto.
XElim H1; Intros
| _ -> Pr0Confluence.
-(*#* #start file *)
-
(*#* #single *)