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

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

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

*** Error 6.5,

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

are uninstantiated type variables

'[_v3_a]'