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

lemma ss_trans: ‹subsequence ys zs ⟹ subsequence xs ys ⟹ subsequence xs zs›