Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
a,a':Assignment. a' extends a
Applied Tactic:
Unfold `extension` 0 THEN Auto
Generated subgoals:
None