proposition: Lemma interp_nlit : forall rho l, interp rho (nlit (blit l)) = negb (Var.interp rho (blit l)).
proof: Proof. unfold nlit;intros rho l;rewrite interp_neg, interp_lit;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring