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

• ```      x : nat
H : {n:nat}(x << (three + n))
?1 : x << three```
will be resolved by Assumption.
• It will however fail with Error: Goal cannot be closed by an instance of any assumption when invoked in the following situation
```      x : nat
H : {n:nat}(n << four)->(x << n)
?1 : x << three```
because a refinement by H would yield the subgoal three << four
• .

## 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