var a : Type

type dummy a := Logical

op b : dummy a

op c : Logical

. c <=> b[a]

. c <=> b;

type

dummy : Type -> Type

type

dummy (a : Type) := Logical

var

a : Type %(var_1)%

op b : forall a : Type . dummy a

op c : Logical

forall a : Type . c <=> b[a]

. c <=> b

1.5: ### Hint: is type variable 'a'

5.10-5.12: ### Hint: is type list '[a]'

6.5:

*** Error: in term '(op c : Logical) <=> (op b : forall a : Type . dummy a)'

are uninstantiated type variables

'[_v3_a]'