case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f✝ f : List α → β
⊢ (permutationsAux2 t [] r [] fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r [] f).snd

case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f✝ : List α → β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β), (permutationsAux2 t [] r tail✝ fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r tail✝ f).snd
f : List α → β
⊢ (permutationsAux2 t [] r (ys_hd :: tail✝) fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r (ys_hd :: tail✝) f).snd
α : Type u_1
β : Type u_2
t : α
ts ys : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r ys fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r ys f).snd
induction' ys with ys_hd _ ys_ih generalizing f
no goals
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f✝ f : List α → β
⊢ (permutationsAux2 t [] r [] fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r [] f).snd
simp
no goals
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f✝ : List α → β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β), (permutationsAux2 t [] r tail✝ fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r tail✝ f).snd
f : List α → β
⊢ (permutationsAux2 t [] r (ys_hd :: tail✝) fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r (ys_hd :: tail✝) f).snd
simp [ys_ih fun xs => f (ys_hd :: xs)]