Inductive ty : Type :=
(* record types *)
| RNil : ty
| RCons : string → ty → ty → ty.
we need typecon to identify record...
Inductive tm : Type :=
| rproj ...? isn't it as well?
(* record terms *)
| rnil : tm
| rcons : string → tm → tm → tm.
``
as a list...
for Record, can compiler reorder the fields? (SML and OCaml)
