proposition: Lemma eval_remove_arrow : forall l st, eval_state st -> eval_state (remove_arrow l st).
proof: Proof. intros. destruct H; constructor ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause