[Dafny] Proving properties on sub sequence

Nov 5, 2012 at 5:58 PM

Hi,

I'm trying to prove all elements in a sub sequence is non-null if all elements in the original sequence is non-null. Here is the program.

http://rise4fun.com/Dafny/T8M

I realize that the same property can be proved on sets since the relations of subsets form a lattice in Dafny.

My question is what is the right way to prove the same property on sub sequences?

Thanks!