proposition: Theorem strong_rec_fixpoint : forall (a : A) (n : N.t), Aeq (strong_rec a f n) (f (strong_rec a f) n).
proof: Proof. intros. transitivity (f (fun n => strong_rec0 a f (S n) n) n). - rewrite strong_rec_alt. apply strong_rec0_fixpoint. - f_equiv. intros x x' Hx; rewrite strong_rec_alt, Hx; auto with *. Qed.
imports: NSub