** Next:** Configure Equality
** Up:** New features in LEGO Version 1.3

# LEGO Version 1.3: Assumption

The command `Assumption` constructs a proof term for the
current goal if it is a (first-order) instance of any of the
current assumptions. `Assumption` `RELGOAL` is an
abbreviation for `Next` `RELGOAL``;
Assumption`.
## Example

## Assumption and Immed

The commands `Try Assumption` and `Immed` are
equivalent in a proof state with a *single* visible goal.
In a proof state with multiple goals, throwing
`Assumption` at a specific goal may well be a better
strategy than invoking `Immed`. The latter tactic may
incorrectly unify some existential variables. It may also take a
*long* time to process. Notice
that `Immed` *never* fails.

LEGO Team
Last modified: Tue Jun 23 16:23:07 BST 1998