proposition: Lemma inhab_ren delta x A: ren delta (inhab x A) = inhab (delta x) A.
proof: Proof. unfold inhab. asimpl. f_equal. f_equal. rewrite it_up_ren_ge; simplify; eauto. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)