proposition: Lemma equiv_app_elim (s s' t t': exp X): s t ≡ s' t' -> isAtom (head s) -> isAtom (head s') -> s ≡ s' /\ t ≡ t'.
proof: Proof. intros (v & [] % steps_app & [] % steps_app) % church_rosser H3; trivial. * do 2 destruct H, H0; intuition idtac; subst; injection H as -> ->; eauto. * do 2 destruct H; destruct H0; intuition idtac; subst. all: destruct (head s'); cbn in *; intuition. * do 2 destruct H0; destruct H; intuition idtac; subst. all: destruct (head s); cbn in *; intuition. * destruct H, H0; intuition idtac. all: destruct (head s); cbn in *; intuition. Qed.
imports: Morphisms Lia FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence)