case intro x h =>
revert h z y
have norm_trans := normalizes_trans _ norm_R
have h :=
  normalizes_ind (. ~>+ .)
  (λ x ↦ ∀ y z, x ~>* y ∧ x ~>* z → y ~>*.*<~ z)
intros y z wedge
(apply h <;> try trivial) <;> try apply norm_trans
clear h
intros x ih y z wedge
cases wedge.1
. exists z; aesop
. case a.step y' red_x_y' red_y'_y =>
  cases wedge.2
  . exists y; aesop
  . case step z' red_x_z' red_z'_z =>
    have join1 := weak _ _ _ red_x_y' red_x_z'
    cases' join1 with w h'
    have join2 : y ~>*.*<~ w :=
    by
      apply ih
      . apply trans_clos.base
        apply red_x_y'
      . aesop
    have join3 : z ~>*.*<~ w :=
    by
      apply ih
      . apply trans_clos.base
        apply red_x_z'
      . aesop
    cases' join2 with w1 h1
    cases' join3 with w2 h2
    have red_x_w : x ~>+ w :=
      by
        apply refl_trans_step_is_trans
        . apply red_x_z'
        . apply h'.2
    have join4 : w1 ~>*.*<~ w2 :=
    by
      apply ih
      . apply red_x_w
      . aesop
     
    cases' join4 with omega h3
    exists omega; constructor
    . apply refl_trans_clos_transitive
      . apply h1.1
      . apply h3.1
    . apply refl_trans_clos_transitive
      . apply h2.1
      . apply h3.2
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
y z x : A
h : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ joins R y z
no goals