Function subrange_of_matching_take 

pub proof fn subrange_of_matching_take<T>(
    a: Seq<T>,
    b: Seq<T>,
    s: int,
    e: int,
    l: int,
)

requires

a[..l] == b[..l],

l <= a.len(),

l <= b.len(),

0 <= s <= e <= l,

ensures

a[s..e] == b[s..e],