Page 321 of 800
| 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 |