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

lemma ss_refl: ‹subsequence ls ls›