Function elaborate_dot 

pub fn elaborate_dot(
    ctx: &Context,
    mctx: &mut MetaCtx,
    receiver: &Term,
    field: &str,
) -> KernelResult<Term>

Elaborate DOT notation receiver.field (E4). The receiver’s type head names an inductive/structure H; the projection is H_field (K4’s convention), applied to H’s parameters — read off the receiver’s type — and then the receiver itself. So p.fst with p : Prod A B becomes Prod_fst A B p. Returns an error if no such projection exists or the result does not type-check.