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