a : bool -> bool

a is not universe polymorphic
Arguments a _%bool_scope
Expands to: Variable a
b : bool -> bool

b is not universe polymorphic
Arguments b _%bool_scope
Expands to: Variable b
negb'' : bool -> bool

negb'' is not universe polymorphic
Arguments negb'' _%bool_scope
negb'' is transparent
Expands to: Constant ArgumentsScope.A.B.negb''
negb' : bool -> bool

negb' is not universe polymorphic
Arguments negb' _%bool_scope
negb' is transparent
Expands to: Constant ArgumentsScope.A.negb'
negb : bool -> bool

negb is not universe polymorphic
Arguments negb _%bool_scope
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
a : bool -> bool

a is not universe polymorphic
Expands to: Variable a
b : bool -> bool

b is not universe polymorphic
Expands to: Variable b
negb : bool -> bool

negb is not universe polymorphic
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
negb' : bool -> bool

negb' is not universe polymorphic
negb' is transparent
Expands to: Constant ArgumentsScope.A.negb'
negb'' : bool -> bool

negb'' is not universe polymorphic
negb'' is transparent
Expands to: Constant ArgumentsScope.A.B.negb''
a : bool -> bool

a is not universe polymorphic
Expands to: Variable a
negb : bool -> bool

negb is not universe polymorphic
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
negb' : bool -> bool

negb' is not universe polymorphic
negb' is transparent
Expands to: Constant ArgumentsScope.negb'
negb'' : bool -> bool

negb'' is not universe polymorphic
negb'' is transparent
Expands to: Constant ArgumentsScope.negb''