(9steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
singelton
append
equals
lemma
T:Type, a:T, R,S:T List, b:T. [a] = (R @ (b.S))
a = b
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
a:
T
3.
R:
T List
4.
S:
T List
5.
b:
T
6.
[a] = (R @ (b.S))
a = b
About:
(9steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc