diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -18,6 +18,8 @@
 typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
   morphisms vec_nth vec_lambda ..
 
+declare vec_lambda_inject [simplified, simp]
+
 notation
   vec_nth (infixl "$" 90) and
   vec_lambda (binder "\<chi>" 10)
@@ -54,7 +56,7 @@
 lemma vec_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> vec_lambda g = f"
   by (auto simp add: vec_eq_iff)
 
-lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g"
+lemma vec_lambda_eta [simp]: "(\<chi> i. (g$i)) = g"
   by (simp add: vec_eq_iff)
 
 subsection \<open>Cardinality of vectors\<close>