proposition: Lemma eval_and_list_eq : forall l, eval_and_list l <-> eval_and_list' l.
proof: Proof. induction l ; simpl. - tauto. - destruct l. + simpl; tauto. + tauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit