Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
n,m:
. n + m
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
. n + m