proposition: Lemma interp_check_lit : forall l1 l2, check_lit l1 l2 -> Lit.interp rho l1 = Lit.interp rho l2.
proof: Proof. unfold check_lit; intros l1 l2; unfold is_true; rewrite !orb_true_iff, !andb_true_iff; intros [[H1|[H1 H2]]|[H1 H2]]. rewrite eqb_spec in H1; rewrite H1; auto with smtcoq_core. rewrite Bool.eqb_true_iff in H1; unfold Lit.interp; rewrite H1, (interp_check_var _ _ H2); auto with smtcoq_core. generalize H1; unfold Lit.interp; case (Lit.is_pos l1); case (Lit.is_pos l2); try discriminate; intros _; unfold Var.interp; rewrite (interp_check_distinct_two_args _ t_func ch_atom ch_form wt_t_atom _ _ H2); auto with smtcoq_core; case (rho (Lit.blit l2)); auto with smtcoq_core. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms