Method only verifies with --useOldAxiomatization

[superaxander]

The following method only seems to verify if I use --useOldAxiomatization:

method lemmaUniquenessPrefix(s1: Seq[Bool], s2: Seq[Bool],
  prefix: Seq[Bool])
  ensures (s1 == s2) == (prefix ++ s1 == prefix ++ s2)
{
  var s3: Seq[Bool]
  var s4: Seq[Bool]
  if (|s1| == |s2|) {
    s3 := prefix ++ s1
    s4 := prefix ++ s2
    inhale (forall y: Int ::
        { s1[y] }
        0 <= y && y < |s1| ==>
        (s1[y] == s2[y]) == (s3[|prefix| + y] == s4[|prefix| + y]))
  }
}