Selected Objects

def	Assignment	Assignment == Var
THM	Assignment_inc	Assignment (Var)
def	restriction	a'a(x) == case (a(x)): 3 (a'(x)); 3 3; 3 (a'(x));
def	extension	a' extends a == a'a = a
THM	extension_lemma	a,a':Assignment. a' extends a (x:Var. a(x) = 3 a(x) = a'(x))