Nuprl - Pf one_one_corr_refl 1 1 1

PrintForm Definitions relation autom Sections AutomataTheory Doc

At: one one corr refl 1 1 1

1. A: Type

InvFuns(A; A; Id; Id)

By: Unfold `inv_funs` 0 THEN Analyze 0 THEN Ext THEN Reduce 0

Generated subgoals:

None

About: