Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:{T
}.
L,M:T List. Dec(L(
eq)M)
Applied Tactic:
D 0 THENA Auto THEN D 0 THENA Auto THEN EquivT (-1) THEN UnivCD THENA Auto
Generated subgoals:
1
. Dec(L(
eq)M)
T:
. eq:{T
}. L,M:T List. Dec(L(
eq)M)eq)M)