proposition: Lemma interp_true : forall rho, Valuation.wf rho -> interp rho _true.
proof: Proof. intros rho Hwf;unfold interp;rewrite is_pos_true, blit_true. apply Var.interp_true;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring