∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (H : Subgroup α) (h : s ≤ t)
  (q₁ q₂ : Quotient (QuotientGroup.leftRel (H.subgroupOf s))),
  Quotient.map' ⇑(Subgroup.inclusion h) ⋯ q₁ = Quotient.map' ⇑(Subgroup.inclusion h) ⋯ q₂ → q₁ = q₂