(*#* #stop file *)

Require subst0_confluence.
Require drop_props.
Require pr0_subst0.
Require pr0_confluence.
Require pr2_defs.

   Section pr2_confluence. (*************************************************)

(* case 1.1 : pr2_free pr2_free *********************************************)

      Remark pr2_free_free: (c:?; t0,t1,t2:?)
                            (pr0 t0 t1) -> (pr0 t0 t2) ->
                            (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
      Intros; Pr0Confluence; XEAuto.
      Qed.

(* case 1.2 : pr2_free pr2_delta ********************************************)

      Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?)
                             (pr0 t0 t1) ->
                             (drop i (0) c (CTail d (Bind Abbr) u)) ->
                             (pr0 t0 t4) ->
			     (subst0 i u t4 t2) ->
                             (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
      Intros; Pr0Confluence; Pr0Subst0; XEAuto.
      Qed.

(* case 2.2 : pr2_delta pr2_delta *******************************************)

      Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,t3,t4,u,u0:?; i,i0:?)
                              (drop i (0) c (CTail d (Bind Abbr) u)) ->
                              (pr0 t0 t3) ->
			      (subst0 i u t3 t1) ->
                              (drop i0 (0) c (CTail d0 (Bind Abbr) u0)) ->
                              (pr0 t0 t4) ->
			      (subst0 i0 u0 t4 t2) ->
                              (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
      Intros; Pr0Confluence; Repeat Pr0Subst0;
      [ XEAuto | XEAuto | XEAuto | Idtac ].
      Apply (neq_eq_e i i0); Intros.
(* case 1 : i != i0 *)
      Subst0Confluence; XEAuto.
(* case 2 : i = i0 *)
      Rewrite H5 in H; Rewrite H5 in H3; Clear H5 i.
      DropDis; Inversion H2; Rewrite H7 in H3; Clear H2 H6 H7 d u.
      Subst0Confluence; [ Rewrite H2 in H0; XEAuto | XEAuto | XEAuto | XEAuto ].
      Qed.

(* main *********************************************************************)

      Hints Resolve pr2_free_free pr2_free_delta pr2_delta_delta : ltlc.

(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap c, t0, t1, t2, t *)

      Theorem pr2_confluence: (c,t0,t1:?) (pr2 c t0 t1) ->
                              (t2:?) (pr2 c t0 t2) ->
                              (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
      Intros; Inversion H; Inversion H0; XDEAuto 3.
      Qed.

   End pr2_confluence.

      Tactic Definition Pr2Confluence :=
         Match Context With
            | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
               LApply (pr2_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | _ -> Pr0Confluence.

(*#* #single *)