proposition: Lemma interp_false : forall rho, Valuation.wf rho -> ~interp rho _false.
proof: Proof. intros rho Hwf;unfold interp;rewrite is_pos_false, blit_false. apply Var.interp_false;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring