proposition: Lemma hconsmap_set_unit_stack : forall l st, hconsmap (set_unit_stack l st) = hconsmap st.
proof: Proof. unfold set_unit_stack. reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause