proposition: Lemma get_pol_None : forall p l, get_pol p l = None -> var l <> p.
proof: Proof. unfold get_pol. intros. destruct (hformula_eqb p (var l)) eqn:E. discriminate. intro. subst. rewrite hformula_eqb_refl in E. discriminate. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Morphisms Cdcl.Lib Cdcl.Syntax