proposition: Theorem example' : forall n, seq' (enumerate n) (cons n (map S (enumerate n))).
proof: Proof. pcofix CIH. intros; pfold. rewrite sunf_eq at 1; simpl. constructor. rewrite (sunf_eq (enumerate n)); simpl. rewrite (sunf_eq (map _ _)); simpl. right; apply CIH. Qed.
imports: Setoid Program Paco.paco