Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
L,M:T List.
eq:{T=
}. L(
eq)M
((
eq) L M)
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. L(
eq)M
((
eq) L M)
T:
. L,M:T List. eq:{T=
}. L(
eq)M 
((eq) L M)eq)M ((eq) L M)