theory Test_Mapper
  imports Main
begin
record ('a,'b) myrec = c1 :: "'a" c2 :: 'b
setup_lifting type_definition_myrec_ext
copy_bnf ('a, 'b, 'm) myrec_ext
term map_myrec_ext
quotient_type ('a,'b) myrec_quot =
 "('a,'b) myrec" / "\<lambda>(r1::('a,'b)myrec) (r2::('a,'b)myrec). c1 r1 = c1 r2"
  by (simp add: equivp_def) metis
end