14.248 At-seqop used for non-free substitution

Prev Up Next 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 ( All #x : A ) at v requires #x to be replaced by v in A. Substitution is done without renaming, so the substitution has to be free (i.e. v must be free for #x in A). As an example, reduction of ( All #x : All #y : #x ) at #y leads to a non-free substitution. The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 719 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05