proposition: Lemma lsteps_cons_inv s t S T: star lstep (s :: S) (t :: T) -> star R s t /\ star 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 (IHstar s' t S T); eauto. + destruct (IHstar s t A' T); eauto. Qed.
imports: List Morphisms FinFun Undecidability.HOU(std.tactics std.ars.basic std.ars.confluence)