proposition: Lemma arity_Arr L A: arity (Arr L A) = length L + arity A.
proof: Proof. induction L; cbn; congruence. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)