∀ {α : Sort u_1} {r : α → α → Prop} {a b c : α},
  (∀ (a b c : α), r a b → r a c → ∃ d, Relation.ReflGen r b d ∧ Relation.ReflTransGen r c d) →
    Relation.ReflTransGen r a b → Relation.ReflTransGen r a c → Relation.Join (Relation.ReflTransGen r) b c