Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
Alph:
.
L,M:L(Alph). L = M
M = L
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
. M = L