10 lines
123 B
Text
10 lines
123 B
Text
|
582.hlean:7:2: proof state
|
||
|
|
A : Type,
|
||
|
|
B : Type,
|
||
|
|
C : Type,
|
||
|
|
f : A → B → C,
|
||
|
|
a : A,
|
||
|
|
b b' : B,
|
||
|
|
p : b = b'
|
||
|
|
⊢ f a b = f a b'
|