1
Set Implicit Arguments.
6
Definition id (A : Set) (x : A) := x.
9
Parameter idid : forall A : Set, A -> A.
13
Definition idid (A : Set) (x : A) := id x.
14
(* <Warning> : Grammar is replaced by Notation *)
15
Notation inc := (plus 1).
18
Definition zero := N.idid 0.
22
Definition zero := M.N.idid 0.
23
Definition jeden := M.N.inc 0.
27
Definition Gole_zero := Goly.idid 0.
28
Definition Goly_jeden := Goly.inc 0.
30
Module Ubrany : M.SIG := M.N.
32
Definition Ubrane_zero := Ubrany.idid 0.