Thms myhill nerode Sections AutomataTheory Doc

aset_car Def a.car == 1of(a)

Thm* T:Type, a:ActionSet(T). a.car Type

pi1 Def 1of(t) == t.1

Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A

About:
!abstractionspreadalluniversefunctionproductmember