Theorem: LO.Modal.Standard.Kripke.Frame.terminal.rel (Logic/Modal/Standard/Kripke/Semantics.lean)

State before:
x y : terminal.World
⊢ x ≺ y ↔ x = y
Tactic:
aesop
State after:
no goals