8 lines
132 B
Text
8 lines
132 B
Text
constant H [intro] : A → B
|
|
constant G [intro] : A → B → C
|
|
constant f [intro] : T → A
|
|
f
|
|
G
|
|
H
|
|
exists_unique.intro
|
|
Exists.intro
|