proposition: Lemma remove_not_correct : forall l, interp_lit (remove_not l) = interp_lit l.
proof: Proof. unfold remove_not;intros l. case_eq (get_form (Lit.blit l));intros;trivial. unfold Lit.interp, Var.interp. rewrite (wf_interp_form interp_atom interp_bvatom t_form default_thf wf_thf (Lit.blit l)), H, interp_Fnot2. destruct(Lit.is_pos l);trivial. rewrite Lit.is_pos_neg, Lit.blit_neg;unfold Lit.interp;destruct (Lit.is_pos i0);trivial. rewrite negb_involutive;trivial. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList