proposition: Lemma eval_or_list_rev : forall l, eval_or_list' (rev l) <-> eval_or_list' l.
proof: Proof. induction l; simpl. - tauto. - rewrite eval_or_list_app. simpl. tauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit