proposition: Lemma Lambda_plus (n m: nat) s: Lambda n (Lambda m s) = Lambda (n + m) s.
proof: Proof. induction n; cbn; congruence. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)