def Qq.inferTypeQ (e : Lean.Expr) : Lean.MetaM ((u : Lean.Level) × (α : let u := u; Q(Sort u)) × Q(«$α»))

instance Qq.instReprMaybeDefEq : {u : Lean.Level} → {α : let u := u; Q(Sort u)} → {a b : Q(«$α»)} → Repr (Qq.MaybeDefEq a b)