Merge pull request #1 from mn200/master

Prove the two-sorts of elements list length lemma
some work done on the integration lemma.
some other work done on the integration lemma.