Require List.

Check List.cons.

Module Modulik.

  Definition T:=nat.

  Export List.

  Check cons.

  Definition x:T:=5.

  Lemma x5 : x=5.
  trivial.
  Qed.

  Hint Resolve x5.

  Notation "!":=x.

  Check !.

Print Hint eq.

Check !.

End Modulik.



Print Hint eq.



Definition T:=bool.

Print Modulik.T.

Print Modulik.

Import Modulik.

Check !.


Check cons.

Locate Module List.

Print Module List.

Print T.

Locate T.

Print Top.T.