proposition: Lemma wf_interp_form : forall x, rho x = Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form.[x]).
proof: Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form). destruct H; intros x;rewrite Form.wf_interp_form;trivial. Qed.
imports: Bool List Int63 PArray State SMT_terms