fact: Definition inhab (x: fin) (A: type) := Lambda (arity A) (@var X (arity A + x)).
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)