proposition: Lemma rho_1: Lit.interp rho 1 = false.
proof: Proof. unfold Lit.interp. unfold Lit.is_pos. simpl. cut (is_even 1 = false). intro Hev. rewrite Hev. unfold Var.interp. destruct wf_rho. unfold Lit.blit. cut (1 >> 1 = 0). intros Heq0. rewrite Heq0. unfold negb. now rewrite H. easy. easy. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance