proposition: Lemma check_atom_correct : wf t_atom -> default t_atom = Acop CO_xH -> forall a1 a2, check_atom a1 a2 -> interp t_i t_func t_atom a1 = interp t_i t_func t_atom a2.
proof: Proof. intros Hwf Hdef;unfold check_atom;apply check_atom_aux_correct; auto. apply check_hatom_correct;trivial. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList