seq_tracked_add

vstd_extra::seq_extra

Function seq_tracked_add 

Source 
pub proof fn seq_tracked_add<T>(s1: Seq<T>, s2: Seq<T>) -> tracked res : Seq<T>
Expand description
ensures
res == s1.add(s2),