work though length_snoc again, finally understand why 1. intros n H (H forced since n comes before) (otherwise the induction hypothesis will have the same n, while it's true for all) 2. destruct n (since ind hyp has an [S n])