proposition: Lemma hconsmap_extract_unit : forall l st st' (EQ : extract_unit st = Some (l, st')), (hconsmap st) = (hconsmap st').
proof: Proof. unfold extract_unit; intros. destruct (unit_stack st) eqn:EQ1; try congruence ; auto. inv EQ. destruct st ; simpl ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause