ext
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
⊢ G.ind univ = G
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
x✝¹ x✝ : α
⊢ (G.ind univ).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝