proposition: Lemma check_hatom_correct_bool : wf t_atom -> default t_atom = Acop CO_xH -> forall h1 h2, check_hatom h1 h2 -> interp_form_hatom t_i t_func t_atom h1 = interp_form_hatom t_i t_func t_atom h2.
proof: Proof. unfold interp_form_hatom; intros H1 H2 h1 h2 H3; rewrite (check_hatom_correct H1 H2 h1 h2 H3); auto. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList