(14steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
fun-graph-rel-graph
2
1.
A:
Type
2.
B:
Type
3.
f:
A
B
A
4.
a:A, b1,b2:B. f(a,b1) = f(a,b2)
b1 = b2
5.
a,a':A. Dec(
b:B. a' = f(a,b))
Bij(A; A; Id)
By:
Easy
Generated subgoals:
None
About:
(14steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc