l,l':Alph*, L,L':LangOver(Alph).
L = L' 
l = l' (L(l) 
L'(l'))
apply_functionality_wrt_lang_eq
Q == (P Q) & (P Q)
Thm* l,l':Alph*, L,L':LangOver(Alph).
L = L' l = l' (L(l) L'(l'))
apply_functionality_wrt_lang_eq
In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 finite sets list 3 autom