proposition: Lemma remove_eq_eq : forall l a a', eq_A a a' -> match (remove eq_bool a l) with | Some l1 => match (remove eq_bool a' l) with | Some l2 => l1 = l2 | None => False end | None => remove eq_bool a' l = None end.
proof: Proof. fix remove_eq_eq 1. intros [ | b l] a a' a_eq_a'; simpl. apply eq_refl. case_eq (eq_bool a b); [intro a_eq_b | intro a_diff_b]. case_eq (eq_bool a' b); [intro a'_eq_b | intro a'_diff_b]. apply eq_refl. apply False_rect. assert (D := eq_bool_ok a' b); rewrite a'_diff_b in D; apply D. transitivity a. symmetry; assumption. assert (E := eq_bool_ok a b); rewrite a_eq_b in E; assumption. case_eq (eq_bool a' b); [intro a'_eq_b | intro a'_diff_b]. apply False_rect. assert (D := eq_bool_ok a b); rewrite a_diff_b in D; apply D. transitivity a'. assumption. assert (E := eq_bool_ok a' b); rewrite a'_eq_b in E; assumption. generalize (remove_eq_eq l _ _ a_eq_a'). case (remove eq_bool a l); case (remove eq_bool a' l); intros; subst; trivial. discriminate. Defined.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)