K semantics (unfinished of course) in K.v

just because I needed something to practice mathcomp