proposition: Lemma permut_list_forall_exists : forall (A B A' B': Type) (R : A -> B -> Prop) (R' : A' -> B' -> Prop) f f', (forall ta ta' tb tb', R ta tb -> R' ta' tb' -> f ta ta' = f' tb tb') -> forall la la' lb lb', permut0 R la lb -> permut0 R' la' lb' -> list_forall (fun t1 => list_exists (fun t2 => f t1 t2) la') la = list_forall (fun t1 => list_exists (fun t2 => f' t1 t2) lb') lb.
proof: Proof. intros A B A' B' R R' f f' E la; induction la as [ | a la]; intros la' lb lb' P P'; inversion P as [ | a' b k1 k2' k2'' a_R_b Q]; subst; simpl; trivial. rewrite list_forall_app; simpl. rewrite (IHla la' (k2' ++ k2'') lb' Q P'). rewrite list_forall_app; simpl. assert (E' : forall (t : A') (t' : B'), R' t t' -> f a t = f' b t'). intros; apply E; trivial. rewrite (@permut_list_exists _ _ R' (fun t2 : A' => f a t2) (fun t2 : B' => f' b t2) E' _ _ P'). destruct (list_exists (fun t2 : B' => f' b t2) lb'); simpl; trivial. destruct (list_forall (fun t1 : B => list_exists (fun t2 : B' => f' t1 t2) lb') k2'); simpl; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)