Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:{T=
}.
L:T List.
x:T. (
M,N:T List. L = M @ (x::N))
x(
eq) L
Applied Tactic:
RepeatFor 2 (D 0 THENA Auto) THEN DiscreteEq (-1) THEN UnivCD THENA Auto
Generated subgoals:
1
.
x(
eq) L
T:
. eq:{T=
}. L:T List. x:T. (
M,N:T List. L = M @ (x::N)) 
x(
eq) Lx(eq) L