Theorem. Rule Induction, Automation, Structured Proofs › compress_expand [isa-002B]

lemma compress_expand:‹well s ⟹ compress (expand s) = s›