proposition: Lemma interp_check_hform : forall h1 h2, check_hform h1 h2 -> Var.interp rho h1 = Var.interp rho h2.
proof: Proof. unfold check_hform; apply foldi_ind; try discriminate. apply leb_0. intros i cont _ _ Hrec h1 h2. unfold is_true; rewrite orb_true_iff; intros [H|H]. rewrite Int63.eqb_spec in H; rewrite H; auto with smtcoq_core. unfold Var.interp; rewrite !wf_interp_form; auto with smtcoq_core; eapply interp_check_form_aux; eauto with smtcoq_core. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms