no goals
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
_x : α
l₁ l₂ : List α
_p : l₁ ~ l₂
r : length l₁ = length l₂
⊢ length (_x :: l₁) = length (_x :: l₂)
simp [r]
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ l₁ l₂ : List α
p : l₁ ~ l₂
_x _y : α
l : List α
⊢ length (_y :: _x :: l) = length (_x :: _y :: l)
simp