Nuprl - Proof: binary ident unique

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A binary operation has at most one identity value.

A:Type, f:(A

A), u,v:A. is_ident(A; f; u)

is_ident(A; f; v)

u = v

By:

Auto

Generated subgoal:

1 1. A : Type
2. f : AAA
3. u : A
4. v : A
5. is_ident(A; f; u)
6. is_ident(A; f; v)
u = v
2 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html