PrintForm Definitions relation autom Sections AutomataTheory Doc

At: one one corr refl 1
1. A: Type

A ~ A
By: Unfold `one_one_corr` 0
Generated subgoal:

1 f,g:(AA). InvFuns(A; A; f; g)

About:
universeexistsfunction