PrintForm Definitions full sequent assignment Sections ClassicalProps(jlc) Doc

At: full sequent assignment properties 1
1. S: Sequent
2. a: Full(S)

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

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

About:
or