Thms myhill nerode Sections AutomataTheory Doc

aset_act Def a.act == 2of(a)

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

pi2 Def 2of(t) == t.2

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

About:
!abstractionspreadalluniversefunctionproductmember