proposition: Lemma eval_and_list_Forall : forall [A:Type] P (l:list A), eval_and_list P l <-> Forall P l.
proof: Proof. intros. rewrite eval_and_list_eq. induction l. - simpl. rewrite Forall_rew. tauto. - simpl. rewrite Forall_rew. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause