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