proposition: Lemma permut_list_exists : forall (A B : Type) (R : A -> B -> Prop) f f', (forall t t', R t t' -> f t = f' t') -> forall l l', permut0 R l l' -> list_exists f l = list_exists f' l'.
proof: Proof. intros A B R f f' E l; induction l as [ | a l]; simpl; intros l' P; inversion P as [ | a' b l1 l2' l2'' a_R_b Q]; subst; simpl; trivial. rewrite list_exists_app; simpl. rewrite (E _ _ a_R_b). destruct (f' b); simpl. destruct (list_exists f' l2'); simpl; trivial. rewrite <- list_exists_app; apply IHl; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)