case nil
α : Type u_1
β : Type ?u.20781
t : α
ts : List α
r : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r [] =
    (List.bind [] fun y => (permutationsAux2 t ts [] y id).snd) ++ r

case cons
α : Type u_1
β : Type ?u.20781
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r (l :: L) =
    (List.bind (l :: L) fun y => (permutationsAux2 t ts [] y id).snd) ++ r
α : Type u_1
β : Type ?u.20781
t : α
ts : List α
r L : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
induction' L with l L ih
no goals
case nil
α : Type u_1
β : Type ?u.20781
t : α
ts : List α
r : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r [] =
    (List.bind [] fun y => (permutationsAux2 t ts [] y id).snd) ++ r
rfl
case cons
α : Type u_1
β : Type ?u.20781
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
⊢ (permutationsAux2 t ts ((List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ ((List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r)
case cons
α : Type u_1
β : Type ?u.20781
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r (l :: L) =
    (List.bind (l :: L) fun y => (permutationsAux2 t ts [] y id).snd) ++ r
simp [ih]
no goals
case cons
α : Type u_1
β : Type ?u.20781
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
⊢ (permutationsAux2 t ts ((List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ ((List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r)
rw [← permutationsAux2_append]