definition bi_confluent (A) (B) (R: bi_relation A B): Prop ≝
∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 →
∃∃a,b. R a1 b1 a b & R a2 b2 a b.
definition bi_confluent (A) (B) (R: bi_relation A B): Prop ≝
∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 →
∃∃a,b. R a1 b1 a b & R a2 b2 a b.