proposition: Theorem compMap_unroll_tl : forall (A B : Set)(def : A)(eqdb : EqDec B)(c : A -> Comp B)(ls : list A) n, length ls = S n -> comp_spec eq (compMap _ c ls) (y <-$ compMap _ c (firstn n ls); x <-$ c (nth n ls def); ret (y ++ x :: nil)).
proof: Proof. induction ls; intuition; simpl in *. lia. destruct n. destruct ls. simpl in *. comp_simp. comp_skip. simpl. eapply comp_spec_eq_refl. simpl in*. lia. simpl. inline_first. comp_skip. eapply comp_spec_eq_trans. eapply comp_spec_seq_eq; eauto with inhabited. intros. eapply comp_spec_eq_refl. inline_first. comp_skip. inline_first. comp_simp. comp_skip. rewrite <- app_comm_cons. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF FCF.CompFold