proposition: Lemma eval_or_list_impl : forall l l', (forall x, In x l' -> exists y, In y l /\ (eval x <-> eval y)) -> eval_or_list l' -> eval_or_list l.
proof: Proof. intros. rewrite! eval_or_list_eq in *. revert l H H0. induction l'; simpl. - tauto. - intros. destruct H0. destruct (H a (or_introl eq_refl)). destruct H1. rewrite H2 in H0. rewrite eval_or_list'_Exists. rewrite Exists_exists. exists x ; tauto. eapply IHl' ; eauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit