proposition: Lemma interp_Fnot2 : forall i l, interp interp_atom interp_bvatom t_form (Fnot2 i l) = interp_lit l.
proof: Proof. intros i l;simpl. apply foldi_ind. apply leb_0. reflexivity. intros; rewrite negb_involutive; assumption. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList