proposition: Lemma wf_pset_singleton : forall hm f, has_form hm f -> wf_pset hm (LitSet.singleton (id f) true).
proof: Proof. constructor. constructor. intros. exists f; split;auto. unfold LitSet.mem,LitSet.singleton in H0. simpl in H0. lia. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause