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

lemma ss_antisym: ‹subsequence ys xs ⟹ subsequence xs ys ⟹ xs = ys›