∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ {inst_1 : DecidableRel G.Adj} [inst_2 : DecidableRel G_1.Adj] {inst_3 : DecidableEq V} [inst_4 : DecidableEq V]
      [inst_5 : AddGroupWithOne R] (a a_1 : V),
      a = a_1 → ∀ (a_2 a_3 : V), a_2 = a_3 → SimpleGraph.lapMatrix R G a a_2 = SimpleGraph.lapMatrix R G_1 a_1 a_3