HOL-Types_To_Sets.Linear_Algebra_On