Thm* a,a':Assignment. a' extends a (x:Var. a(x) = 3 a(x) = a'(x)) extension_lemma
In prior sections: core bool 1 rel 1 sqequal 1 prog 1 int 2 list 1 bool 2 jlc core 3 jlc list 3 jlc Three