## 8.4.6 Arbitrary terms

Page 321 of 800 |
| Search internet |

The following constructs allow to say that some metavariable V denotes an arbitrary term:

line L : Arbitrary >> V ; N

Example:

In Line L01 we state that denotes an arbitrary variable.

Using 'arbitrary' is the typical way to prove a lemma of form .

Do not use 'arbitrary' in proof of form

T proof of L : P qed

where T is Prop, FOL, or Peano from the Peano page. The tactics of Prop, FOL, and Peano are not intended to be used together with meta-quantification.

Page 321 of 800 |
| Search logiweb.eu |

Copyright © 2010
Klaus Grue,
GRD-2010-01-05