add lemmas about seq

Adding a couple of lemmas about seq. Please let me know if you prefer bigger MRs. I have a fair amount of stuff that I want to merge eventually.