Linked List insertion in Dafny

LinkedList.dfy

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 := 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()
    }
}