Use seqs instead of map for env for wf rules...

... to be well-founded. maps are not yet ranked wrt to datatypes in
dafny... (my todo!)
lemma1
lemma2

refactored pmap to use an inductive data type. easier for the proofs.