Nuprl - Proof: identity-biject

T:Type. Bij(T; T; Id)

By: Unfold `biject` 0 THEN Unfolds [`inject`;`surject`] 0 THEN Reduce 0 THEN Obvious

Generated subgoals:

None

About: