Collapse a theorem representing a single definition into a single line.
DESCRIPTION
Given a theorem which describes equations for a single constant, derive a
reformulation where any pattern matching clauses have been combined and
replaced by a single case expression. This produces a left-hand side
consisting of the constant applied only to variables.
USES
To advance a proof by unfolding a function defined by pattern-matching, but
where the pattern is not yet constrained enough.
EXAMPLE
> listTheory.MAP;
val it = ⊢ (∀f. MAP f [] = []) ∧ ∀f h t. MAP f (h::t) = f h::MAP f t: thm
> oneline it;
val it = ⊢ MAP f v = case v of [] => [] | h::t => f h::MAP f t: thm
FAILURE
Fails on theorems of the wrong form, including definition of multiple constants.