proposition: Lemma consts_inhab x A: consts (inhab x A) === nil.
proof: Proof. unfold inhab; rewrite consts_Lam; reflexivity. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)