proposition: Lemma list_equiv_ind (P: list X -> list X -> Prop): P nil nil -> (forall s t S T, equiv R s t -> equiv lstep S T -> P S T -> P (s :: S) (t :: T)) -> forall S T, equiv lstep S T -> P S T.
proof: Proof. intros B IH S T H; induction S in T, H |-*; destruct T; trivial. - exfalso; eapply not_equiv_lstep_nil_cons; eauto. - exfalso; eapply not_equiv_lstep_nil_cons; symmetry; eauto. - eapply equiv_lstep_cons_inv in H as (? & ?). eapply IH; eauto. Qed.
imports: List Morphisms FinFun Undecidability.HOU(std.tactics std.ars.basic std.ars.confluence)