∀ {V : Type u} [inst : FirstOrder.Language.graph.Structure V],
  V ⊨ FirstOrder.Language.Theory.simpleGraph ↔
    (Std.Irrefl fun x y => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]) ∧
      Symmetric fun x y => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]