. have h' := ih joins_y_z
  trivial
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R b✝ z
no goals