proposition: Lemma wf_remove_arrow : forall e st, wf_state st -> wf_state (remove_arrow e st).
proof: Proof. intros. destruct H; constructor ; auto. unfold remove_arrow. simpl. apply Forall_removeb ;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause