proposition: Lemma remove_arrow_correct : forall e st, wf_state st -> wf_state (remove_arrow e st) /\ (eval_state st -> eval_state (remove_arrow e st)) /\ (eval_annot_state st -> eval_annot_state (remove_arrow e st)) /\ hconsmap (remove_arrow e st) = hconsmap st.
proof: Proof. intros. destruct H. split_and. - constructor ; auto. unfold remove_arrow. simpl. apply Forall_removeb; auto. - intro H ; destruct H ; constructor ; auto. - intro H ; destruct H ; constructor ; auto. - reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause