case mk
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ { val := xs, property := (_ : List.length xs = List.length xs) }) =
    Seq.seq (cons <$> f x) fun x => Vector.traverse f { val := xs, property := (_ : List.length xs = List.length xs) }
n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
x : α
⊢ ∀ (xs : Vector α n), Vector.traverse f (x ::ᵥ xs) = Seq.seq (cons <$> f x) fun x => Vector.traverse f xs
rintro ⟨xs, rfl⟩
no goals
case mk
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ { val := xs, property := (_ : List.length xs = List.length xs) }) =
    Seq.seq (cons <$> f x) fun x => Vector.traverse f { val := xs, property := (_ : List.length xs = List.length xs) }
rfl