α : Type u
L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ List.length L1 + List.length L2 + 2 = List.length L1 + List.length ((x, b) :: (x, !b) :: L2)
α : Type u
L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ List.length (L1 ++ L2) + 2 = List.length (L1 ++ (x, b) :: (x, !b) :: L2)
rw [List.length_append, List.length_append]
no goals
α : Type u
L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ List.length L1 + List.length L2 + 2 = List.length L1 + List.length ((x, b) :: (x, !b) :: L2)
rfl