proposition: Lemma wf_union : forall s s' (WFT: wf s) (WFT': wf s'), wf (union s s').
proof: Proof. unfold union. intros. apply IntMap.wf_xcombine'; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause