instance instInhabitedQuotedDefEq_iris {u✝ : Lean.Level} {α✝ : Q(Sort u✝)} {a b : Q($α✝)} : Inhabited («$a» =Q «$b»)

Equations

• instInhabitedQuotedDefEq_iris = { default := ⋯ }