class List
{
  var value:int;
  var next:List;
  
  predicate inv { acc(value) && acc(next) && (next!=null ==> next.inv) }
  
  function get():int
    requires inv;
  { unfolding inv in value }
  
  method foo()
    requires inv && unfolding inv in next!=null;
	ensures inv && unfolding inv in next!=null;
  {
    assert unfolding inv in unfolding next.inv in true;
  }
}