Level: Lib Thy Top: 1
Hypotheses:

  1. n :

  2. m :

Conclusion:

n + m

Applied Tactic: D 2 THEN D 1 THEN MemTypeCD THEN Auto'
Generated subgoals:

None