ext x
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
⊢ l = l'
case h
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
x : X
⊢ l x = l' x