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