proposition: Lemma equiv_neq_const_lam s c: ~ const c ≡ lambda s.
proof: Proof. intros (v & ? & ?) % church_rosser; trivial. inv H; firstorder idtac using normal_var. eapply steps_lam in H0 as []; intuition idtac; discriminate. inv H1. Qed.
imports: Morphisms Lia FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence)