proposition: Lemma remove_4_aux : forall m (Hm:Sort m) x y, ~ eq x y -> In y m -> In y (remove x m).
proof: Proof. intros m Hm x y; generalize Hm; clear Hm. induction m as [ |[k' x0] l IHf]; simpl; [ |case_eq (compare x k'); intros _x e1];subst;auto with smtcoq_array; match goal with | [H: compare _ _ = _ |- _ ] => clear H | _ => idtac end. rewrite In_alt. inversion_clear 3; auto with smtcoq_array. inversion H2. unfold eqk in H3. simpl in H3. subst. now contradict H0. apply In_alt. exists x. auto with smtcoq_array. apply lt_not_eq in _x. intros. inversion_clear Hm. inversion_clear H0. unfold MapsTo in H3. apply InA_eqke_eqk in H3. unfold In. destruct (eq_dec k' y). exists x0. apply InA_cons_hd. split; simpl; auto with smtcoq_array. inversion H3. unfold eqk in H4. simpl in H4; subst. now contradict n. assert ((exists e : elt, MapsTo y e (remove x l)) -> (exists e : elt, MapsTo y e ((k', x0) :: remove x l))). intros. destruct H6. exists x2. apply InA_cons_tl. auto with smtcoq_array. apply H6. apply IHf; auto with smtcoq_array. apply In_alt. exists x1. auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance