proposition: Lemma check_atom_correct : forall t_atom, check_atom t_atom -> wf t_atom /\ default t_atom = Acop CO_xH.
proof: Proof. intro t_atom; unfold check_atom; case (default t_atom); try discriminate; intro c; case c; auto; discriminate. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList