coq eval strategy

(* nが偶数の時nat,奇数の時boolを返す *)
Fixpoint tf (n:nat):Set:=
match n with
| O => nat
| S O => bool
| S (S n0) => tf n0
end.
(* 上と同じものを再定義 *)
Fixpoint tf2 (n:nat):Set:=
match n with
| O => nat
| S O => bool
| S (S n0) => tf2 n0
end.
(*これは当然動く*)
Definition t1
(f: (tf (100*100*10))->nat )
(x: (tf (100*100*10)) )
:= f x.
(*なぜか意外と動く*)
Definition t2
(f: (tf (100*100*10))->nat )
(x: (tf2 (100*100*10)) )
:= f x.
(*なぜか意外と動く*)
Definition t3
(f: (tf (100*10*100))->nat )
(x: (tf2 (100*100*10)) )
:= f x.
(*時間が掛かるがなぜか意外と動く*)
Definition t3
(f: (tf (100*100*10+2))->nat )
(x: (tf (100*100*10)) )
:= f x.
(*NG判定が動かない*)
Definition t3
(f: (tf (100*100*10+1))->nat )
(x: (tf (100*100*10)) )
:= f x.