proposition: Lemma units_set_unit_stack: forall s st, units (set_unit_stack s st) = units 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