simp [copyCount, isContained_iff_exists_subgraph, card_pos, filter_eq_empty_iff]
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
⊢ G.copyCount H = 0 ↔ ¬G ⊑ H
no goals