proposition: Lemma eval_or_list_dec : forall l, Forall (fun x => eval x \/ ~ eval x) l -> eval_or_list l \/ ~ eval_or_list l.
proof: Proof. intros. induction H. - simpl. tauto. - simpl. destruct l. tauto. tauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit