proposition: Lemma valid_check_micromega : forall cl c, C.valid rho (check_micromega cl c).
proof: Proof. unfold check_micromega; intros cl c. case_eq (build_clause empty_vmap cl). intros (vm1, bf) Heq. destruct (build_clause_correct _ _ _ _ Heq). red;simpl;auto with smtcoq_core. decompose [and] H0. case_eq (ZTautoChecker bf c);intros Heq2. unfold C.valid;rewrite H5. apply ZTautoChecker_sound with c;trivial. apply C.interp_true. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form);trivial. intros _;apply C.interp_true. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form);trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz