proposition: Lemma nth_force_rec': forall n (f g: nat -> T) i, n<=i -> nth g i (force_rec f nil n) = g O.
proof: Proof. induction n; intros f g i H. case i; reflexivity. rewrite force_rec_rec. destruct i. inversion H. simpl. apply IHn. auto with arith. Qed.
imports: Coq(List) Coq(Arith)