proposition: Lemma eval_op_list_cons : forall o e l, eval_op_list o (e::l) <-> eval_lop o (eval e) (eval_op_list o l).
proof: Proof. destruct o; unfold eval_op_list; intros. - rewrite! eval_and_list_eq. simpl ; tauto. - rewrite! eval_or_list_eq. simpl ; tauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit