proposition: Lemma Exists_rew : forall {A: Type} [P: A -> Prop] l, Exists P l <-> match l with | nil => False | a::l => P a \/ Exists P l end.
proof: Proof. split ; intros. - inv H; tauto. - destruct l. tauto. destruct H. apply Exists_cons_hd; auto. eapply Exists_cons_tl;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause