simp [GeachConfluent, Symmetric]
α : Sort ?u.505
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 0, j := 0, m := 1, n := 1 } F ↔ Serial F.Rel
α : Sort ?u.505
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x : F.World}, ∃ u, x ≺ u) ↔ Serial F.Rel