∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (H : Subgroup α) (h : s ≤ t) (a b : ↥s),
  (QuotientGroup.leftRel (H.subgroupOf s)) a b →
    (QuotientGroup.leftRel (H.subgroupOf t)) ((Subgroup.inclusion h) a) ((Subgroup.inclusion h) b)