∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g h k : G} {a b c : α} (hg : b = g • a)
  (hh : c = h • b) (hk : c = k • a),
  k = h * g →
    (MulAction.stabilizerEquivStabilizer hg).trans (MulAction.stabilizerEquivStabilizer hh) =
      MulAction.stabilizerEquivStabilizer hk