α : Type u_1
β : Type ?u.26869
t : α
ts is : List α
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) ts (t :: is))
      (is ::
        permutationsAux.rec (fun x => [])
          (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) is []) =
    foldr (fun y r => (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) ts (t :: is))
      (permutations is)
α : Type u_1
β : Type ?u.26869
t : α
ts is : List α
⊢ permutationsAux (t :: ts) is =
    foldr (fun y r => (permutationsAux2 t ts r y id).snd) (permutationsAux ts (t :: is)) (permutations is)
rw [permutationsAux, permutationsAux.rec]
no goals
α : Type u_1
β : Type ?u.26869
t : α
ts is : List α
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) ts (t :: is))
      (is ::
        permutationsAux.rec (fun x => [])
          (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) is []) =
    foldr (fun y r => (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) ts (t :: is))
      (permutations is)
rfl