[Dafny] Proving properties on sub sequence

Nov 5, 2012 at 5:58 PM


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.


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?