proposition: Lemma wf_empty : forall m, wf m -> wf_state (empty_state m).
proof: Proof. constructor ; simpl;auto. - apply wf_map_empty;auto. - apply wf_units_def_empty. - unfold wf_units_lit. intros. rewrite empty_o in H0. congruence. - unfold has_clauses. apply WMap.Forall_empty. - apply wf_map_empty;auto. - apply WMap.wf_empty. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause