proposition: Lemma valid_check_distinct_elim : forall input, C.valid rho input -> forall res, C.valid rho (check_distinct_elim input res).
proof: Proof. induction input as [ |l c IHc]; auto with smtcoq_core; simpl; unfold C.valid; simpl; rewrite orb_true_iff; intros [H|H] res. case_eq (check_lit' l res); intro Heq; simpl. rewrite <- (interp_check_lit' _ _ Heq), H; auto with smtcoq_core. rewrite H; auto with smtcoq_core. case (check_lit' l res). simpl; rewrite H, orb_true_r; auto with smtcoq_core. simpl; rewrite (IHc H), orb_true_r; auto with smtcoq_core. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms