node always
  (i: bool)
returns
  (o: bool);

var
  V4_prev: bool;

let
  o = (if i then V4_prev else false);
  V4_prev = (true -> (pre o));
tel