proposition: Lemma wf_unit_or : forall m r (HFr : has_form m r), Forall (has_literal m) (unit_or r).
proof: Proof. unfold unit_or. intros. destruct (elt r); constructor ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause