∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ (r r_1 : ℕ),
      r = r_1 →
        ∀ (k k_1 : ℕ),
          k = k_1 →
            ∀ (v v_1 : α),
              v = v_1 →
                ∀ (w₁ w₁_1 : α),
                  w₁ = w₁_1 →
                    ∀ (w₂ w₂_1 : α),
                      w₂ = w₂_1 →
                        ∀ (s s_1 : Finset α),
                          s = s_1 →
                            ∀ (t t_1 : Finset α),
                              t = t_1 →
                                G.IsFiveWheelLike r k v w₁ w₂ s t = G_1.IsFiveWheelLike r_1 k_1 v_1 w₁_1 w₂_1 s_1 t_1