case nil
α : Type u_1
β : Type ?u.7760
t : α
⊢ permutations'Aux t [] = (permutationsAux2 t [] [[] ++ [t]] [] id).snd

case cons
α : Type u_1
β : Type ?u.7760
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd
α : Type u_1
β : Type ?u.7760
t : α
ts : List α
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
induction' ts with a ts ih
case cons
α : Type u_1
β : Type ?u.7760
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).snd =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun x => a :: x).snd
case cons
α : Type u_1
β : Type ?u.7760
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd
simp [permutations'Aux, permutationsAux2_snd_cons, ih]
case cons
α : Type u_1
β : Type ?u.7760
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) ((permutationsAux2 t [] [] ts id).snd ++ [ts ++ [t]]) =
    (permutationsAux2 t [] [] ts fun x => a :: x).snd ++ [a :: (ts ++ [t])]
case cons
α : Type u_1
β : Type ?u.7760
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).snd =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun x => a :: x).snd
simp (config := { singlePass := true }) only [← permutationsAux2_append]
no goals
case cons
α : Type u_1
β : Type ?u.7760
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) ((permutationsAux2 t [] [] ts id).snd ++ [ts ++ [t]]) =
    (permutationsAux2 t [] [] ts fun x => a :: x).snd ++ [a :: (ts ++ [t])]
simp [map_permutationsAux2]
no goals
case nil
α : Type u_1
β : Type ?u.7760
t : α
⊢ permutations'Aux t [] = (permutationsAux2 t [] [[] ++ [t]] [] id).snd
rfl