Theorem. Rule Induction, Automation, Structured Proofs › Length of subsequence [isa-002E]

lemma ss_length : ‹subsequence xs ys ⟹ length xs ≤ length ys›