Fixpoint has_non_trivial_constr ls :=
	match ls with
	| nil => false
	| cons x xs =>
		if x == Constructor []
		then has_non_trivial_constr xs
		else true
	end

Defintion IsEnumeration type :=
	match Reflect(type) with
	| InductiveType ls => not (has_non_trivial_constr ls)
	end.

Fixpoint compare_constr type1 type2 ls1 ls2 :=
	match ls1, ls2 with
	| nil, _ => false
	| _, nil => true
	| x::xs, y::ys =>
			if x <> y && (x <> type1 || y <> type2)
			then false
			else compare_constr type1 type2 xs ys

Fixpoint compare_constrs type1 type2 ls1 ls2 :=
	match ls1, ls2 with
	| nil, _ => true
	| _, nil => false
	| (Constructor x)::xs, (Constructor y)::ys => (compare_constr type1 type2 x y) && (compare_constrs type1 type2 xs ys)
	end.

Definition BinaryCompatible type1 type2 :=
	match Reflect(type1) Reflect(type2) with
	| InductiveType ls1, InductiveType ls2 => compare_constrs type1 type2 ls1 ls2
	end.