proposition: Lemma equiv_Lambda_elim k s t: Lambda k s ≡ Lambda k t -> s ≡ t.
proof: Proof. induction k; cbn; eauto using equiv_lam_elim. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)