proposition: Lemma get_pol_inv : forall p l b, get_pol p l = Some b -> l = make b p.
proof: Proof. unfold get_pol. intros. destruct (hformula_eqb p (var l)) eqn:E. inv H. apply hformula_eqb_true in E. subst. apply decomp. discriminate. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Morphisms Cdcl.Lib Cdcl.Syntax