intro h
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
⊢ (∀ (i : ι), Adj (s i) x y) → ¬x = y
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
h : ∀ (i : ι), Adj (s i) x y
⊢ ¬x = y