Page 718 of 800
| Page 718 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
Substitution of x with v produces non-meta-term
As an example, substitution of 
by 
in 
yields the illformed metaterm 
. The error may indicate an error in the proof or a bug in a tactic.
| Page 718 of 800 | Search logiweb.eu |