I expect the following to type check: ``` -- Main.juvix module Main; axiom X : Type; axiom x' : X; axiom x : X; f : X := let x : X := x'; in Main.x; ```