(9steps)
PrintForm
list
3
jlc
Sections
Support(jlc)
Doc
At:
singelton
append
equals
lemma
1
1
2
1.
T:
Type
2.
a:
T
3.
b:
T
4.
u:
T
5.
v:
T List
6.
[a] = b.v
a = b
7.
[a] = [b; u/ v]
a = b
By:
ApFunToHypEquands `L' (Case of L; nil
a ; h.t
h) T -1
THEN
Reduce -1
Generated subgoals:
None
About:
(9steps)
PrintForm
list
3
jlc
Sections
Support(jlc)
Doc
a = b
a = b
a ; h.t h) T -1
