proposition: Lemma beval_clause_app : forall env l1 l2, beval_clause env (l1 ++ l2) = (beval_clause env l1 || beval_clause env l2).
proof: Proof. induction l1; simpl. - reflexivity. - intros. rewrite IHl1. btauto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit