proposition: Lemma strong_rec_any_fst_arg : forall a a' n, Aeq (strong_rec a f n) (strong_rec a' f n).
proof: Proof. intros a a' n. generalize (le_refl n). set (k:=n) at -2. clearbody k. revert k. pattern n. apply induction; clear n. - intros n n' Hn. setoid_rewrite Hn; auto with *. - intros k Hk. rewrite le_0_r in Hk. rewrite Hk, strong_rec_0. symmetry. apply strong_rec_0_any. - intros n IH k Hk. rewrite 2 strong_rec_fixpoint. apply step_good. intros m Hm. apply IH. rewrite succ_le_mono. apply le_trans with k; auto. rewrite le_succ_l; auto. Qed.
imports: NSub