no goals
α : Type ?u.105001
β : Type ?u.105004
γ : Type ?u.105007
n : ℕ
⊢ ¬last n ∈ map castSucc.toEmbedding univ
simp [map_eq_image]
no goals
α : Type ?u.105001
β : Type ?u.105004
γ : Type ?u.105007
n : ℕ
⊢ univ = cons (last n) (map castSucc.toEmbedding univ) (_ : ¬last n ∈ map castSucc.toEmbedding univ)
simp [map_eq_image]