proposition: Lemma eval_op_list_app : forall o l1 l2, eval_op_list o (l1++l2) <-> eval_lop o (eval_op_list o l1) (eval_op_list o l2).
proof: Proof. destruct o; simpl;intros. - rewrite! eval_and_list_eq. rewrite eval_and_list_app. tauto. - rewrite! eval_or_list_eq. rewrite eval_or_list_app. tauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit