constructor
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX ∧ ¬confluent RX
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX

case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX