dafny sequence to multiset

While trying to make some assertions about sequences and subsequences I came to realize that dafny does not seem to prove this statement. I don't know how it could not be true. Should I just make this an axiom and move on or this there a way to prove this to dafny?

lemma multisetSequence(nums: seq<int>, ms: multiset<int>) 
    requires |nums| > 0
    requires multiset(nums[1..]) == ms;
    ensures multiset(nums) == ms + multiset{nums[0]}
{
    assert forall i :: 1 <= i < |nums| ==> nums[i] in ms;
    assert forall i :: 1 <= i < |nums| ==> nums[i] in multiset(nums);
    //the following fails, which breaks my brain
    assert forall i :: 1 <= i < |nums| && nums[i] != nums[0] ==> multiset(nums)[nums[i]] == ms[nums[i]];
    if nums[0] in ms {
        assert multiset(nums)[nums[0]] == ms[nums[0]]+1;
    }else{
        assert ms[nums[0]] == 0;
        assert multiset(nums)[nums[0]] == 1;
    }
}

I think you're going down a rabbit hole. The issue is simply sequence extentionality on nums:

This verifies for me:

lemma multisetSequence(nums: seq<int>, ms: multiset<int>) 
    requires |nums| > 0
    requires multiset(nums[1..]) == ms;
    ensures multiset(nums) == ms + multiset{nums[0]}
{
  assert nums == [nums[0]] + nums[1..];
}