proposition: Lemma in_remove : forall a l, match remove a l with | None => ~mem a l | Some l' => {a' : A & {l' : list A & {l'' : list A | eqA a a' /\ l = l' ++ a' :: l'' /\ remove a l = Some (l' ++ l'')}}} end.
proof: Proof. intros a l; functional induction (remove a l) as [ l l_eq_nil | l a' l' l_eq_a'_l' a_eq_a' | l a' l' l_eq_a'_l' a_diff_a' IH rmv H | l a' l' l_eq_a'_l' a_diff_a' IH H]. intros a_in_nil; contradiction. exists a'; exists (@nil A); exists l'; simpl; repeat split; trivial. generalize (eq_bool_ok a a'); rewrite a_eq_a'; trivial. rewrite H in IH; revert IH; intros [a'' [l'' [l''' [H' [H'' H''']]]]]. exists a''; exists (a' :: l''); exists l'''; subst l'; rewrite app_comm_cons; injection H'''; intros; subst. simpl; intuition. rewrite H in IH. simpl; intros [a_eq_a' | a_in_l']. generalize (eq_bool_ok a a'); rewrite a_diff_a'; intro Abs; apply Abs; assumption. apply (IH a_in_l'); trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)