proposition: Lemma interp_check_lit' : forall l res, check_lit' l res -> Lit.interp rho l = Lit.interp rho res.
proof: Proof. apply interp_check_lit, interp_check_hform; auto with smtcoq_core. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms