Theorem: LO.Modal.Standard.Kripke.GeachConfluent.terminal_frame (Logic/Modal/Standard/Kripke/Geach/Definability.lean)

State before:
α : Sort ?u.253943
inst✝ : Inhabited α
F : Frame
t : Geach.Taple
⊢ GeachConfluent t Frame.terminal.toFrame
Tactic:
simp [GeachConfluent, Frame.terminal.relItr.mpr]
State after:
no goals