proposition: Lemma compMap_length : forall (A : Type)(B : Set)(eqd : EqDec B)(ls : list A) x (c : A -> Comp B) , In x (getSupport (compMap _ c ls)) -> length x = length ls.
proof: Proof. induction ls ; intuition. simpl in *. intuition; subst. simpl. trivial. unfold compMap in *. fold compMap in *. repeat simp_in_support. simpl. f_equal. eauto. Qed.
imports: FCF.FCF Permutation