proposition: Lemma compMap_support : forall (A B : Set)(P : A -> B -> Prop)(eqd : EqDec B)(c : A -> Comp B)(lsa : list A)(lsb : list B), In lsb (getSupport (compMap _ c lsa)) -> (forall a b, In a lsa -> In b (getSupport (c a)) -> P a b) -> list_pred P lsa lsb.
proof: Proof. induction lsa; intuition. simpl in *. intuition; subst. econstructor. unfold compMap in *. fold compMap in *. repeat simp_in_support. econstructor. eapply H0. simpl. intuition. trivial. eapply IHlsa. trivial. intuition. Qed.
imports: FCF.FCF Permutation