DISP	Assignment_df	Assignment== Assignment
ABS	Assignment	Assignment == Var
THM	Assignment_wf	Assignment
THM	Assignment_inc	Assignment Var
DISP	restriction_df	<a:Assignment:*><a':Assignment:*>== <a><a'>
ABS	restriction	a'a == x.case (a x): 3 (a' x); 3 3; 3 (a' x);
THM	restriction_wf	a',a:Assignment. a'a Assignment
DISP	extension_df	<a':Assignment:*> extends <a:Assignment:*>== <a'> extends <a>
ABS	extension	a' extends a == a'a = a
THM	extension_wf	a,a':Assignment. a' extends a
THM	extension_lemma	a,a':Assignment. a' extends a (x:Var. (a x = 3) a x = a' x)

the other theories