PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
one
one
corr
symm
A,B:Type. (A ~ B)
(B ~ A)
By:
Unfold `one_one_corr` 0
THEN
GenExRepD
Generated subgoal:
1
1.
A:
Type
2.
B:
Type
3.
f:
A
B
4.
g:
B
A
5.
InvFuns(A; B; f; g)
f:(B
A), g:(A
B). InvFuns(B; A; f; g)
About:
BA
f:(BA), g:(AB). InvFuns(B; A; f; g) 
A,B:Type. (A ~ B) 
(B ~ A)BA f:(BA), g:(AB). InvFuns(B; A; f; g)
