simp [or_and_right, exists_or, ih]
case h₂
V✝ : Type u_1
V' : Type u_2
G : SimpleGraph V✝
K : Type u_3
K' : Type u_4
ι : Type u_5
V : Type u_6
f : ι → SimpleGraph V
x y : V
a : ι
s : Finset ι
has : a ∉ s
ih : Adj (sup s f) x y ↔ ∃ i ∈ s, Adj (f i) x y
⊢ Adj (sup (cons a s has) f) x y ↔ ∃ i ∈ cons a s has, Adj (f i) x y
no goals