proposition: Lemma Lambda_injective n (s t: exp X): Lambda n s = Lambda n t -> s = t.
proof: Proof. induction n; cbn; intuition; eapply IHn; congruence. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)