assignment
Sections
ClassicalProps(jlc)
Doc
Def
a' extends a == a'
a = a
Thm*
a,a':Assignment. a' extends a
(
x:Var.
a(x) = 3
a(x) = a'(x)) extension_lemma
a,a':Assignment. a' extends a 
(x:Var. 
a(x) = 3
a(x) = a'(x))
extension_lemma
a = a
a,a':Assignment. a' extends a (x:Var. a(x) = 3 a(x) = a'(x))
extension_lemma