pub fn loop_invariant_ty() -> Expr
LoopInvariant: the invariant for a while loop. Type: (State → Prop)