proposition: Lemma interp_check_form : forall a b, check_form a b -> Form.interp interp_form_hatom interp_form_hatom_bv t_form a = Form.interp interp_form_hatom interp_form_hatom_bv t_form b.
proof: Proof. apply interp_check_form_aux, interp_check_hform; auto with smtcoq_core. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms