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