Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

P,Q:. {P Q} {Dec(P) Dec(Q)}

Applied Tactic: Unfolds ``guard decidable`` 0 THEN Auto
Generated subgoals:

1. Q Q

2. P P