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