proposition: Lemma order_union_l : forall b b', order b (union b b').
proof: Proof. destruct b,b'; simpl; auto. destruct (Bool.eqb b b0) eqn:E; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause