proposition: Theorem compMap_head : forall (A: Type)(B : Set)(eqd : EqDec B)(f : A -> Comp B)(ls : list A) x, (forall a, In a ls -> well_formed_comp (f a)) -> evalDist (ls' <-$ compMap _ f ls; ret (head ls')) x == evalDist (match (head ls) with | None => ret None | Some a => b <-$ f a; ret (Some b) end) x.
proof: Proof. destruct ls; intuition. unfold compMap. unfold hd_error. unfold error. comp_simp. intuition. unfold compMap. fold compMap. unfold hd_error. fold hd_error. unfold value. inline_first. comp_skip. inline_first. comp_irr_l. eapply compMap_wf. intuition. intuition. Qed.
imports: FCF.FCF Permutation