Dear PVS users: I do not know how to prove the following goal: |------- {1} length(append(l1!1, l2!1)) = length(l1!1) + length(l2!1) where l1!1, l2!1 are of type list[int]. Did anyone know how to prove it? Many thanks. -- Jei-Wen Teng