proposition: Lemma subset_union_l : forall s s', wf_map s -> wf_map s' -> subset s (union s s').
proof: Proof. unfold subset,union,get, wf_map. intros. rewrite IntMap.gxcombine' with (opt:=None); auto. change (option bool) with OBool.t. destruct (IntMap.get' k s) ; simpl. destruct (IntMap.get' k s'). apply OBool.order_union_l. apply OBool.order_refl. destruct (IntMap.get' k s') ; simpl; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause