proposition: Lemma set_env_same : forall {A:Type} env p (v:A), set_env env p v p = v.
proof: Proof. unfold set_env. intros. destruct (hformula_eq_dec p p);try congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause