proposition: Theorem removeFirst_In_length : forall (A : Set)(eqd : EqDec A)(ls : list A)(a : A), In a ls -> length (removeFirst (EqDec_dec _ ) ls a) = pred (length ls).
proof: Proof. induction ls; intuition; simpl in *. intuition; subst. destruct (EqDec_dec eqd a0 a0); intuition. destruct (EqDec_dec eqd a0 a); subst. trivial. simpl. rewrite IHls. destruct ls; simpl in *; intuition. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation