Fix semantics/proofs

Except for 2 lemmas about bootstrapping in evalPropsScript