clear h
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
h :
  (∀ (x : A),
      (∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z) →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ ∀ (x : A),
    (∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z) →
      ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ ∀ (x : A),
    (∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z) →
      ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z