proposition: Theorem compMap_unroll : forall (A B : Set)(eqdb : EqDec B)(c : A -> Comp B)(ls : list A)(def : A), ls <> nil -> comp_spec eq (compMap _ c ls) (x <-$ c (hd def ls); y <-$ compMap _ c (tl ls); ret (x :: y)).
proof: Proof. induction ls; intuition; simpl in *. comp_skip. Qed.
imports: FCF.FCF FCF.CompFold