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