Set Primitive Projections.
Record c : Type := { fst : nat; snd : fst = 0 }.
Search concl:fst.