Function borrow_prophecy_var 

pub proof fn borrow_prophecy_var<'a, 'b, T: ?Sized>(
    tracked m: &'a &'b mut T,
) -> tracked t : &'a ProphecyGhost<&'b T>

ensures

t.value() == &*final(*m),