proposition: Lemma eqb_map_correct : forall {A: Type} (f: A -> bool) m m', eqb_map f m m' = true -> m = IntMap.map1' f m'.
proof: Proof. unfold eqb_map. induction m. - destruct m'; simpl; solve[reflexivity|discriminate]. - destruct m'; simpl; try (reflexivity||discriminate). intros. apply andb_true_iff in H. destruct H. apply eqb_correct in H. rewrite Bool.eqb_true_iff in H0. congruence. - simpl. destruct m'; simpl; try (reflexivity||discriminate). intros. rewrite! andb_true_iff in H. destruct H as (((P1 & P2) & P3) & P4). apply eqb_correct in P1. apply eqb_correct in P2. subst. f_equal; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause