proposition: Lemma eval_insert_defs : forall m' a st, eval_state st -> eval_state (insert_defs m' a st).
proof: Proof. intros. destruct H. unfold insert_defs. constructor ; simpl ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause