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 Require Export termination.

Local confluence / confluence

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

Local confluence.
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.


Confluence.
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.