proposition: Lemma eval_and_list'_Forall : forall l, eval_and_list' l <-> Forall eval l.
proof: Proof. induction l. - simpl. rewrite Forall_rew. tauto. - simpl. rewrite Forall_rew. tauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit