proposition: Lemma remove_4 : forall m (Hm:Sort m) x y, ~ eq x y -> In y m <-> In y (remove x m).
proof: Proof. split. apply remove_4_aux; auto. revert H. generalize Hm; clear Hm. functional induction (remove x m);subst;auto; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac end. intros. destruct H0 as (e, H0). exists e. apply InA_cons_tl. auto. intros. apply lt_not_eq in _x. inversion_clear Hm. apply In_inv in H0. destruct H0. exists x0. apply InA_cons_hd. split; simpl; auto. specialize (IHf H1 H H0). inversion IHf. exists x1. apply InA_cons_tl. auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance