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