Constructor prefixed with t_ in rec bundle

[maximebuyse]

mod a {
    pub struct S(pub i32);
    pub fn f() -> S{super::b::g()}
}

mod b {
    pub fn g() -> super::a::S {
        super::a::S(0)
    }
}

Open this code snippet in the playground

Here in the generated fstar the constructor of S in g is called t_S instead of just S