simp [EdgeInd']
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => ↑(EdgeInd' (G ω) e)) ⊆ {0, 1}
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => if Edge (G ω) e then 1 else 0) ⊆ {0, 1}