case trans x y z red_x_y red_y_z joins_x_y joins_y_z =>
  cases' joins_x_y with w1 h1
  cases' h1 with h11 h12
  cases' joins_y_z with w2 h2
  cases' h2 with h21 h22
  have h' : wedge R w1 w2 := by
    exists y
  have h := confl w1 w2 h'
  cases' h with w h''
  exists w; cases' h'' with h3 h4
  constructor <;> apply refl_trans_clos_transitive <;> trivial
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
joins_x_y : joins R x y
joins_y_z : joins R y z
⊢ joins R x z
no goals