proposition: Lemma eval_and_list_impl : forall l l', (forall x, In x l -> exists y, In y l' /\ (eval x <-> eval y)) -> eval_and_list l' -> eval_and_list l.
proof: Proof. intros. rewrite! eval_and_list_eq in *. revert l' H H0. induction l; simpl. - intuition. - intros. split. destruct (H a (or_introl eq_refl)). destruct H1. rewrite H2. clear H2. revert x H1. rewrite <- Forall_forall. apply eval_and_list'_Forall in H0 ; auto. eapply IHl ; eauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit