proposition: Lemma interp_neg : forall rho l, interp rho (neg l) = negb (interp rho l).
proof: Proof. intros rho l;unfold interp;rewrite is_pos_neg, blit_neg. destruct (is_pos l);simpl;auto using negb_involutive. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring