proposition: Lemma has_bool_union : forall b o1 o2, (has_bool b o1 \/ has_bool b o2) <-> has_bool b (union o1 o2).
proof: Proof. unfold has_bool. destruct o1, o2; simpl ; intuition. - rewrite Bool.eqb_true_iff in H0. subst. destruct (Bool.eqb b0 b1) eqn:E;simpl;auto. apply Bool.eqb_reflx. - rewrite Bool.eqb_true_iff in H0. subst. destruct (Bool.eqb b0 b1) eqn:E;simpl;auto. rewrite Bool.eqb_true_iff in *. congruence. - destruct (Bool.eqb b0 b1) eqn:E;simpl in H ; try congruence. + apply eqb_prop in E. subst. tauto. + simpl in *. destruct b;destruct b0 ; destruct b1 ; simpl in *; intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause