Thm* a,a':Assignment. a' extends a (x:Var. a(x) = 3 a(x) = a'(x)) extension_lemma
In prior sections: Three
a,a':Assignment. a' extends a 
(x:Var. 
a(x) = 3
a(x) = a'(x))
extension_lemma
== inr(inl(
))
a,a':Assignment. a' extends a (x:Var. a(x) = 3 a(x) = a'(x))
extension_lemma