Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
P,Q:
. Dec(P)
Dec(Q)
{
(P
Q)
P
Q}
Applied Tactic:
GenUnivCD THENA Auto
Generated subgoals:
1
.
(P
Q)
P
Q
P,Q:
. Dec(P) 
Dec(Q) {
(P 
Q) 
P 
Q}(P Q) P Q