proposition: Lemma lit_interp_true : Lit.interp rho Lit._true = true.
proof: Proof. apply Lit.interp_true. apply wf_rho. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance