proposition: Lemma compMap_support_app : forall (A: Type)(B : Set)(eqd : EqDec B)(c : A -> Comp B)(lsa1 lsa2 : list A)(lsb1 lsb2 : list B), In lsb1 (getSupport (compMap _ c lsa1)) -> In lsb2 (getSupport (compMap _ c lsa2)) -> In (lsb1 ++ lsb2) (getSupport (compMap _ c (lsa1 ++ lsa2))).
proof: Proof. induction lsa1; intuition. simpl in H. intuition; subst. repeat rewrite app_nil_l. trivial. unfold compMap in H. fold compMap in H. repeat simp_in_support. repeat rewrite <- app_comm_cons. unfold compMap. fold compMap. eapply getSupport_In_Seq; eauto. eapply getSupport_In_Seq; eauto. simpl; intuition. Qed.
imports: FCF.FCF Permutation