Page 719 of 800
| Page 719 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
At-seqop used for non-free substitution. Attempt to instantiate x with v
Reduction of 
requires 
to be replaced by 
in 
. Substitution is done without renaming, so the substitution has to be free (i.e. must be free for in ). As an example, reduction of 
leads to a non-free substitution. The error may indicate an error in the proof or a bug in a tactic.
| Page 719 of 800 | Search logiweb.eu |