proposition: Lemma mem_union : forall k s s' (WFT: wf s) (WFT': wf s'), (mem k s = true \/ mem k s' = true) <-> mem k (union s s') = true.
proof: Proof. unfold mem, union. intros. repeat rewrite IntMap.gmem'. rewrite IntMap.gxcombine' with (opt:=None) ; auto. change (option bool) with OBool.t. destruct (IntMap.get' k s). destruct (IntMap.get' k s') ; auto. simpl. intuition congruence. simpl. intuition congruence. destruct (IntMap.get' k s') ; simpl ; intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause