2 lines
106 B
Text
2 lines
106 B
Text
def f : {x : A} → {x_1 : B x} → {c : @C x x_1} → @D x x_1 c → Bool :=
|
|
fun {x} {x_1} {c} d => true
|