proposition: Lemma equiv_lstep_cons_inv s t S T: equiv lstep (s :: S) (t :: T) -> equiv R s t /\ equiv lstep S T.
proof: Proof. intros H. remember (s :: S) as S'. remember (t :: T) as T'. revert s t S T HeqS' HeqT'. induction H; intros. - subst. injection HeqT' as ??; subst; intuition. - subst. inv H. + destruct x'. eapply lstep_cons_nil in H1 as []. edestruct IHstar; trivial. inv H1. * intuition idtac. transitivity x; eauto. * intuition idtac. transitivity x'; eauto. + destruct x'. eapply lstep_nil_cons in H1 as []. edestruct IHstar; trivial. inv H1; intuition idtac. * transitivity x; eauto. * transitivity x'; eauto. Qed.
imports: List Morphisms FinFun Undecidability.HOU(std.tactics std.ars.basic std.ars.confluence)