let the (x : U) (a : x) : x = a; -- Introduce typed parameter in this way can help minitt better infer the -- types