apply conf' <;> aesop
case a.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : trans_clos R x z
⊢ joins R y z
no goals