xyx-is

## Coq_match_strange_error.v
Inductive vect (a:Set) :forall b:Type, a -> b -> Type:=
 | vnilt (x:a) b (y:b) : vect a b x y.
Definition tmp:=vnilt nat 1 bool true.
Check tmp. (* vect nat bool 1 true *)
Definition tmp2:nat :=match tmp with z => 1 end. (* error *)

## 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
	Inductive vect (a:Set) :forall b:Type, a -> b -> Type:=
	\| vnilt (x:a) b (y:b) : vect a b x y.
	Definition tmp:=vnilt nat 1 bool true.
	Check tmp. (* vect nat bool 1 true *)
	Definition tmp2:nat :=match tmp with z => 1 end. (* error *)
	(* 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