simp [GeachConfluent, Symmetric]
α : Sort ?u.13729
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 0, j := 1, m := 0, n := 1 } F ↔ Symmetric F.Rel
α : Sort ?u.13729
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z ≺ y) ↔ ∀ ⦃x y : F.World⦄, F.Rel x y → F.Rel y x