Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:{T=
}.
P:T
.
x:T.
L:T List.
x(
eq) L
P[x]
y
L.P[y]
Applied Tactic:
RepeatFor 5 (D 0 THENA Auto)
Generated subgoals:
1
.
x(
eq) L
P[x]
y
L.P[y]
T:
. eq:{T=
}. P:T 
. x:T. L:T List. 
x(
eq) L 
P[x] 
yL.P[y]x(eq) L P[x] yL.P[y]