proposition: Lemma map_Ret_repeat : forall (A : Set)(eqd : eq_dec A)(a : A) ls ls', rel_map (evalDet (Ret eqd a)) ls ls' -> ls' = listRepeat (ca_done a) (length ls).
proof: Proof. induction ls; inversion 1; intuition; subst; simpl in *. f_equal. inversion H4; clear H4; subst. inversion H0; clear H0; subst. simpl in *. inversion H6; clear H6; subst. trivial. inversion H0; clear H0; subst; simpl in *. inversion H6. inversion H; clear H; subst. eapply IHls. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat