Function vstd::seq_lib::lemma_append_last

source · 
pub proof fn lemma_append_last<A>(s1: Seq<A>, s2: Seq<A>)
Expand description
requires
0 < s2.len(),
ensures
(s1 + s2).last() == s2.last(),

The last element of two concatenated sequences, the second one being non-empty, will be the last element of the latter sequence.