Questions: It seems that ToMS() does not maintain the info from the Sequence.

[RabbitDong-on]

I try to verify the equivalence between two sorted sequences. My idea is (1) verfiy s1[0]==s2[0] and then (2) recursively verify s1.drop(1)==s2.drop(1). However, I fail to leverage an important condition ( ToMS(s1)==ToMS(s2) ).

def sorted_equivalence_lemma(s1:PSeq[int],s2:PSeq[int])->bool:
    Requires(len(s1)==len(s2) and len(s1)==1)
    Requires(ToMS(s1)==ToMS(s2))
    Requires(Forall(int, lambda i:(Implies(i>=0 and i<len(s1)-1,s1[i]<=s1[i+1]))))
    Requires(Forall(int, lambda i:(Implies(i>=0 and i<len(s2)-1,s2[i]<=s2[i+1]))))
    Ensures(s1==s2)
    
    if len(s1)==len(s2) and len(s1)==0:
        return True
    elif len(s1)==len(s2) and len(s1)==1:
        if s1[0] == s2[0]:
            Assert(s1[0]==s2[0])
            s3=s1.take(1)
            s4=s2.take(1)
            # Assert(ToMS(s1)==ToMS(s2))
            # Assert(len(ToMS(s1)-ToMS(s2))==0)
            # Assert(ToMS(s3)==ToMS(s1))
            # Assert(ToMS(s4)==ToMS(s2))
            Assert(ToMS(s3)==ToMS(s4))
            Assert(s1==s2)
            return True
        else:
            Assert(ToMS(s1)==ToMS(s2))
            return False
    elif len(s1)==len(s2) and len(s1)>1:
        if s1[0]==s2[0]:
            Assert(s1[0]==s2[0])
            # Assert(ToMS(s1)==ToMS(s2))
            # drops1=PSeq(s1[0])
            # drops2=PSeq(s2[0])
            # Assert(ToMS(s1)==ToMS(s2))
            # Assert(ToMS(drops2)==ToMS(drops1))
            # Assert((ToMS(s1)-ToMS(drops1))==(ToMS(s2)-ToMS(drops2)))
            Assert(ToMS(s1.drop(1))==ToMS(s2.drop(1)))
            return sorted_equivalence_lemma(s1.drop(1),s2.drop(1))
        else:
            Assert(ToMS(s1)==ToMS(s2))
            return False

First, i try to verify the simplest case, i.e., len(s1)==1. However, I get some error messages. I am not sure how to use ToMS(s1)==ToMS(s2) to guarantee that the elements in two sorted sequences are the same. Specifically, when len(s1)==1, how to use ToMS(s1)==ToMS(s2) to tell verifer elements in two sequences are the same? (instead of 0 and False)
Error messages

Verification failed
Errors:
Assert might fail. Assertion (s1 == s2) might not hold. (learn_example.py@153.19--153.25).
Old store:
  s1 -> Sequence: { len(s1) -> 1, s1[0] -> False },
  s2 -> Sequence: { len(s2) -> 1, s2[0] -> 0 }
Old heap: Empty.
Current store:
  s3 -> Sequence: { len(s3) -> 1, s3[0] -> False },
  s4 -> Sequence: { len(s4) -> 1, s4[0] -> 0 },
  s1 -> Sequence: { len(s1) -> 1, s1[0] -> False },
  s2 -> Sequence: { len(s2) -> 1, s2[0] -> 0 },
  Result() -> ?
Current heap: Empty.

Verification took 38.03 seconds.

Questions: How to use ToMS(s1)==ToMS(s2) to guarantee that the elements in two sorted sequences are the same?
Any suggestions are greatly appreciated. This issue is related to #222