{| field := 5 |}
     : test
{| field := 5 |}
     : test
{| field_r := 5 |}
     : test_r
build_c 5
     : test_c
build 5
     : test
build 5
     : test
{| field_r := 5 |}
     : test_r
build_c 5
     : test_c
fun '(C _ p) => p
     : N -> True
fun '{| T := T |} => T
     : N -> Type
fun '(C T p) => (T, p)
     : N -> Type * True
fun '{| q := p |} => p
     : M -> True
fun '{| U := T |} => T
     : M -> Type
fun '{| U := T; q := p |} => (T, p)
     : M -> Type * True
fun '{| U := T; a := a; q := p |} => (T, p, a)
     : M -> Type * True * nat
fun '{| U := T; a := a; q := p |} => (T, p, a)
     : M -> Type * True * nat