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