case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
⊢ length (permutations'Aux x []) = length [] + 1

case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
x y : α
s : List α
IH : length (permutations'Aux x s) = length s + 1
⊢ length (permutations'Aux x (y :: s)) = length (y :: s) + 1
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
⊢ length (permutations'Aux x s) = length s + 1
induction' s with y s IH
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
⊢ length (permutations'Aux x []) = length [] + 1
simp
no goals
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
x y : α
s : List α
IH : length (permutations'Aux x s) = length s + 1
⊢ length (permutations'Aux x (y :: s)) = length (y :: s) + 1
simpa using IH