def Lean.Elab.mkInhabitantFor (declName : Lake.Name) (xs : Array Lean.Expr) (type : Lean.Expr) : Lean.MetaM Lean.Expr