[GOAL]
X : Type u
inst✝¹ : Preorder X
inst✝ : OrderTop X
x : X
a : x ⟶ ⊤
⊢ a = default
[PROOFSTEP]
rfl
[GOAL]
X : Type u
inst✝¹ : Preorder X
inst✝ : OrderBot X
x : X
a : ⊥ ⟶ x
⊢ a = default
[PROOFSTEP]
rfl
