PrintForm Definitions full assignment Sections ClassicalProps(jlc) Doc

At: full formula assignment properties 1
1. F: Formula
2. a: Full(F)

a |= F a | F
By:
UnfoldTopAb -1
THEN
Analyze -1
Generated subgoal:

12. a: Assignment
3. a |= F a | F
a |= F a | F

About:
or