∀ {V : Type u_1} (G : SimpleGraph V) (x x_1 : V ⊕ V),
  (fun x x_2 =>
        match x, x_2 with
        | Sum.inl v', Sum.inr w' => G.Adj v' w'
        | Sum.inr v', Sum.inl w' => G.Adj v' w'
        | x, x_3 => False)
      x x_1 →
    (fun x x_2 =>
        match x, x_2 with
        | Sum.inl v', Sum.inr w' => G.Adj v' w'
        | Sum.inr v', Sum.inl w' => G.Adj v' w'
        | x, x_3 => False)
      x_1 x