Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:{T
}.
t:T.
L:T List.
t(
eq) (t::L)
Applied Tactic:
AbReduce 0 THEN UnivCD THENA Auto
Generated subgoals:
1
.
if eq t t then tt else t(
eq) L fi
T:
. eq:{T
}. t:T. L:T List. 
t(
eq) (t::L)if eq t t then tt else t(eq) L fi