proposition: Theorem compMap_fold_equiv : forall (A:Type)(B : Set)(eqd : EqDec B)(c : A -> Comp B)(ls : list A), comp_spec eq (compMap eqd c ls) (compMap_fold eqd c ls).
proof: Proof. induction ls; intuition; simpl. unfold compMap_fold. simpl. eapply comp_spec_eq_refl. unfold compMap_fold. simpl. prog_inline_first. prog_skip. prog_simp. eapply comp_spec_eq_trans. eapply comp_spec_seq_eq; eauto with inhabited. intuition. eapply comp_spec_eq_refl. unfold compMap_fold. eapply comp_spec_eq_trans_r. 2:{ eapply comp_spec_right_ident. } eapply comp_spec_seq; eauto with inhabited. eapply (@compFold_spec _ _ _ (fun ls p1 p2 => b :: p1 = p2)); intuition. subst. simpl. comp_skip. eapply comp_spec_ret. trivial. intuition. subst. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF