assignment Sections ClassicalProps(jlc) Doc

Def == Unit+Unit+Unit

Thm* a,a':Assignment. a' extends a (x:Var. a(x) = 3 a(x) = a'(x)) extension_lemma

Thm* Assignment (Var) Assignment_inc

In prior sections: Three