proposition: Lemma check_neg_hatom_correct_bool : wt t_i t_func t_atom -> wf t_atom -> default t_atom = Acop CO_xH -> forall h1 h2, check_neg_hatom h1 h2 -> interp_form_hatom t_i t_func t_atom h1 = negb (interp_form_hatom t_i t_func t_atom h2).
proof: Proof. unfold interp_form_hatom. intros Hwt H1 H2 h1 h2 H3. unfold interp_bool. generalize (check_neg_hatom_correct Hwt H1 H2 _ _ H3). case (interp_hatom t_i t_func t_atom h1). case (interp_hatom t_i t_func t_atom h2). simpl. intros [ |i| | | | ] v1 [ |j| | | | ] v2; intro H; inversion H. rewrite Typ.cast_refl. auto. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList