MarkB
generic
Sections
NuprlLIB
Doc
Def
agree_on_common(T;as;bs) == Case of as; nil
True ; a.as'
Case of bs; nil
True ; b.bs'
(a
bs) & agree_on_common(T;as';bs)
(b
as) & agree_on_common(T;as;bs')
a = b
T & agree_on_common(T;as';bs') (recursive)
is mentioned
In prior sections:
mb
list
1
mb
list
2
MarkB
generic
Sections
NuprlLIB
Doc
True ; a.as' 
(a 
bs) & agree_on_common(T;as';bs) 