Errors.out

File "./output/Errors.v", line 12, characters 0-11:
The command has indeed failed with message:
The field t is missing in Errors.M.
File "./output/Errors.v", line 19, characters 18-19:
The command has indeed failed with message:
Unable to unify "nat" with "True".

File "./output/Errors.v", line 20, characters 12-15:
The command has indeed failed with message:
Unable to unify "nat" with
 "True".
In nested Ltac calls to "f" and "apply x", last call failed.

File "./output/Errors.v", line 29, characters 21-30:
The command has indeed failed with message:
Instance is not well-typed in the environment of ?x.
Ltac call to "instantiate ( (ident) := (lglob) )" failed.

File "./output/Errors.v", line 34, characters 19-20:
The command has indeed failed with message:
Cannot infer ?T in the partial instance "?T -> nat" found for the type of f.
File "./output/Errors.v", line 35, characters 22-24:
The command has indeed failed with message:
Cannot infer ?T in the partial instance "?T -> nat" found for the implicit
parameter A of id whose type is "Type".
File "./output/Errors.v", line 36, characters 17-18:
The command has indeed failed with message:
Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the
type of f in environment:
x : nat
File "./output/Errors.v", line 44, characters 5-23:
The command has indeed failed with message:
The first term has type "nat" while the second term has incompatible type
"bool".

File "./output/Errors.v", line 49, characters 7-24:
The command has indeed failed with message:
Replacement would lead to an ill-typed term: Illegal application: 
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
 "Set" : "Type"
 "n" : "Type"
 "n" : "Type"
The 2nd term has type "Type" which should be a subtype of 
"Set". (universe inconsistency: Cannot enforce Errors.35 <= Set)