Dafny链表指定位置插入节点验证报错，求排查方案

我参考Rustan Leino的论文完成了链表队列的验证工作，现尝试实现更通用的队列插入功能——在指定位置插入节点而非仅追加。参考资料编写代码后，最终断言报错，无法证明next in footprint与next.valid()。我怀疑valid谓词定义存在问题，同时也不清楚如何合理推导contents的更新逻辑，恳请提供帮助。

class Node {
    var data: int
    var next: Node?
    
    ghost var footprint: set<object>
    ghost var contents: seq<int>
    
    ghost predicate valid()
        reads this, footprint
    {
        this in footprint &&
        (next != null ==> next in footprint &&
            next.footprint <= footprint &&
            this !in next.footprint &&
            next.valid()) &&
        (next == null ==> |contents| == 0 &&
            next != null ==> next.contents == contents[1..])
    }
    
    constructor()
        modifies this
        ensures valid() && fresh(footprint - {this})
        ensures next == null
        ensures |contents| == 0
    {
        next := null;
        contents := [];
        footprint := {this}
    }
    
    method enqueueMid(d: int, pos: int)
        requires valid()
        requires 0 <= pos <= |contents|
        modifies footprint
        ensures valid() && fresh(footprint - old(footprint))
    {
        var i: int := 0;
        var curr := this;
        
        while(i < pos && curr.next != null)
            invariant curr != null
            invariant curr != null ==> curr.valid()
            decreases if curr != null then curr.footprint else {}
        {
            i := i + 1;
            curr := curr.next;
        }
        
        var n := new Node();
        n.data := d;
        
        if(curr == null) {
            curr := n;
            contents := contents + [d]; // if current is null then we have reached the end of the list!
        } else {
            n.next := curr.next;
            n.footprint := curr.footprint - {curr}; // acyclicity!
            curr.footprint := curr.footprint + n.footprint;
            curr.next := n;
            contents := contents[ .. pos] + [d] + contents[pos ..];
        }
        
        footprint := footprint + n.footprint;
        assert(valid()); // error: could not prove: next in footprint. could not prove: next.valid()
    }
}

内容的提问来源于stack exchange，提问作者Drona Nagarajan