proposition: Lemma equiv_head_equal X (s t: exp X): s ≡ t -> isAtom (head s) -> isAtom (head t) -> head s = head t.
proof: Proof. induction s in t |-*; destruct t; intros; try Discriminate; Injection H; subst; trivial. - cbn in *; intuition idtac. - cbn; eapply IHs1; eauto. Qed.
imports: Morphisms Lia FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence)