α : Type u_1
β : Type ?u.19875
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys fun x => [] ++ x).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
α : Type u_1
β : Type ?u.19875
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys id).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
rw [show @id (List α) = ([] ++ .) by funext _; rfl]
no goals
α : Type u_1
β : Type ?u.19875
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys fun x => [] ++ x).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
apply mem_permutationsAux2
case h
α : Type u_1
β : Type ?u.19875
t : α
ts ys l x✝ : List α
⊢ id x✝ = [] ++ x✝
α : Type u_1
β : Type ?u.19875
t : α
ts ys l : List α
⊢ id = fun x => [] ++ x
funext _
no goals
case h
α : Type u_1
β : Type ?u.19875
t : α
ts ys l x✝ : List α
⊢ id x✝ = [] ++ x✝
rfl