proposition: Lemma fold_left_None_None : forall [A B: Type] (F : option A -> B -> option A) (FN : forall a, F None a = None), forall l, fold_left F l None = None.
proof: Proof. induction l; simpl ; auto. rewrite FN. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause