Locally Confluent Terminating to Confluent

theorem LocallyConfluent.Terminating_toConfluent (hlc : LocallyConfluent r) (ht : Terminating r) :    Confluent r := by  intro x  induction x using ht.induction with  | h x ih =>    intro y z xy xz    cases xy.cases_head with    | inl => exists z; grind    | inr h =>      obtain ⟨y₁, x_y₁, y₁_y⟩ := h      cases xz.cases_head with      | inl => exists y; grind      | inr h =>        obtain ⟨z₁, x_z₁, z₁_z⟩ := h        have ⟨u, z₁_u, y₁_u⟩ := hlc x_z₁ x_y₁        have ⟨v, uv, yv⟩ : Join (ReflTransGen r) u y := by grind        have ⟨w, vw, zw⟩ : Join (ReflTransGen r) v z := by grind [ReflTransGen.trans]        exact ⟨w, .trans yv vw, zw⟩