Accept record projections without requiring type in `Top`

[oskgo]

MRE of current error:

theory T.
type t= {f: unit}.
op e: t.
end T.
op test = T.e.`f.

I believe the following is an example of how this is currently being worked around.

easycrypt/examples/UC/dh_enc.ec

Lines 215 to 216 in b09b7ae

	(* This is a hack *)
	op kstp st = st.`kst.

The code already works if t is present in the top level scope:

theory T.
type t= {f: unit}.
op e: t.
end T.
import T.
op test = T.e.`f.

theory T.
type t.
op e: t.
end T.
type t' = {f: unit}.
clone T as T' with type t <- t'.
op test = T'.e.`f.