PrintForm
Definitions
elimination
Sections
ClassicalProps(jlc)
Doc
At:
formula
not
left
sound
1
1
1
1.
concl:
Formula List
2.
M:
Formula List
3.
N:
Formula List
4.
f2:
Formula
5.
a:
Full( < M @ (
f2.N),concl > )
a
Full( < M @ N,f2.concl > )
By:
Unfold `full_sequent_assignment` 0
Generated subgoal:
1
a
{a:Assignment| a |= < M @ N,f2.concl >
a |
< M @ N,f2.concl > }
About:
a 
{a:Assignment| a |= < M @ N,f2.concl > 
a |
< M @ N,f2.concl > }
f2.N),concl > ) a Full( < M @ N,f2.concl > ) a {a:Assignment| a |= < M @ N,f2.concl > a | < M @ N,f2.concl > }
