proposition: Lemma build_formula_correct : forall h' vm vm' f, build_formula vm h' = Some (vm',f) -> wf_vmap vm -> wf_vmap vm' /\ (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ (forall p, (nat_of_P p < nat_of_P (fst vm))%nat -> nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_formula (fst vm') f /\ (interp_form_hatom h' <-> Zeval_formula (interp_vmap vm') isProp f).
proof: Proof. unfold build_formula;intros h. unfold Atom.interp_form_hatom, Atom.interp_hatom. rewrite t_interp_wf;trivial. intros;apply build_formula_atom_correct with (get_type t_i t_func t_atom h);trivial. unfold wt, is_true in wt_t_atom;rewrite aforallbi_spec in wt_t_atom. case_eq (h <? length t_atom);intros Heq;unfold get_type;auto with smtcoq_core. unfold get_type'. rewrite !PArray.get_outofbound, default_t_interp, def_t_atom;trivial; try reflexivity. rewrite length_t_interp;trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz