Require Import Omega.
Require Export Setoid Morphisms Equivalence.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Coq.Program.Equality.
Require Export ARS.
From Chapter4 Require Export termination.

Ltac instantiate_IH :=
  match goal with
  | [H : equiv_axiom ?s ?t, H' : forall u, equiv_axiom ?s _ -> _ |- _] => destruct (H' _ H) as (?&?&?)
  | [H : equiv_axiom_subst ?s ?t, H' : forall u, equiv_axiom_subst ?s _ -> _ |- _] => destruct (H' _ H) as (?&?&?)
  end.

Lemma equiv_locally_confluent :
  locally_confluent equiv_axiom /\ locally_confluent equiv_axiom_subst.
Proof with (repeat (try auto_inv; eauto 10)).
  apply comb_equiv_ind; intros...
  all: try (instantiate_IH; eauto 20).
  all: eauto 20.
Qed.

Lemma equiv_confluent :
  confluent equiv_axiom /\ confluent equiv_axiom_subst.
Proof.
  split; apply newman; try apply equiv_locally_confluent.
  all: eauto using sn_exp, sn_subst.
Qed.