proposition: Lemma get_or_correct : forall l args, get_or l = Some args -> interp_lit l = interp interp_atom interp_bvatom t_form (For args).
proof: Proof. unfold get_or;intros l args. rewrite <- remove_not_correct;unfold Lit.interp;generalize (remove_not l). intros l';unfold Var.interp. destruct (Lit.is_pos l');[ | discriminate]. rewrite wf_interp_form;trivial. destruct (get_form (Lit.blit l'));intros Heq;inversion Heq;trivial. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList