myhill
nerode
Sections
AutomataTheory
Doc
inject
Def
Inj(A; B; f) ==
a1,a2:A. f(a1) = f(a2)
B
a1 = a2
Thm*
A,B:Type, f:(A
B). Inj(A; B; f)
Prop
About:
a1,a2:A. f(a1) = f(a2) 
B 
a1 = a2
A,B:Type, f:(A
B). Inj(A; B; f) Propa1,a2:A. f(a1) = f(a2) B a1 = a2
