-
Notifications
You must be signed in to change notification settings - Fork 1
Open
Labels
Description
The following proof script incorrectly results in the last line in the box being rendered as P(x) when it should be P(y0).
%abbrev
ex2-3-6-a : {P}
proof (all ([x] P x) , |- all ([y] P y)) =
[P]
all ([x] P x) premise; [@prem]
( var[y0]
P y0 by all_e y0 @prem
) ; [box]
all ([y] P y) by all_i box.
Reactions are currently unavailable