no goals
α : Type ?u.106203
β : Type ?u.106206
γ : Type ?u.106209
n : ℕ
p : Fin (n + 1)
⊢ ¬p ∈ map (succAbove p).toEmbedding univ
simp
no goals
α : Type ?u.106203
β : Type ?u.106206
γ : Type ?u.106209
n : ℕ
p : Fin (n + 1)
⊢ univ = cons p (map (succAbove p).toEmbedding univ) (_ : ¬p ∈ map (succAbove p).toEmbedding univ)
simp [map_eq_image]