∀ {α : Type u_4} (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst : DecidableRel G.Adj} [inst_1 : DecidableRel G_1.Adj] (s s_1 : Finset α),
      s = s_1 → ∀ (t t_1 : Finset α), t = t_1 → G.interedges s t = G_1.interedges s_1 t_1