λ(x : { c : Natural }) → x.{ c } ⫽ { a = 1 }