proposition: Lemma lift_has_bool_union : forall b i d1 d2 (WFT: wf d1) (WFT': wf d2), (OBool.lift_has_bool b (get i d1) \/ OBool.lift_has_bool b (get i d2) ) <-> OBool.lift_has_bool b (get i (union d1 d2)).
proof: Proof. intros. unfold get, union, OBool.lift_has_bool. rewrite IntMap.gxcombine' with (opt:=None) ; auto. change (option bool) with OBool.t. destruct (IntMap.get' i d1). - simpl. destruct (IntMap.get' i d2) ; auto. apply OBool.has_bool_union. simpl. intuition congruence. - simpl. destruct (IntMap.get' i d2) ; simpl; intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause