Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
a:Assignment.
q,r:Formula. a |
q
r
a |= q
a |
r
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. a |
q
r
a |= q
a |
r
a:Assignment. q,r:Formula. a |
q
r 
a |= q 
a | r qr a |= q a | r