proposition: Lemma lit_interp_false : Lit.interp rho Lit._false = false.
proof: Proof. specialize (Lit.interp_false rho wf_rho). intros. rewrite <- not_true_iff_false. unfold not in *. intros. now apply H. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance