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