proposition: Lemma eval_or_app : forall {A: Type} (F: A-> Prop) l1 l2, eval_or F (l1++l2) <-> (eval_or F l1 \/ eval_or F l2).
proof: Proof. induction l1;simpl. - tauto. - intros. rewrite IHl1. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause