\newlabel{ded-eqv}{{A.1}{17}}
\newlabel{inv-ca}{{A.2}{17}}
\newlabel{v-smpsc}{{A.3}{18}}
\newlabel{app-vdash-decidable}{{A.4}{18}}
\newlabel{v-red-nc}{{A.5}{20}}
\newlabel{or-confl}{{A.6}{20}}
\newlabel{v-red-alt}{{A.7}{22}}
\newlabel{v-nf-no-left}{{A.8}{22}}
\newlabel{v-red-pair-enc}{{A.9}{22}}
\newlabel{v-reduce}{{A.10}{23}}
\newlabel{a-sms}{{A.11}{23}}
\newlabel{v-l-Ne}{{A.12}{23}}
\newlabel{v-is-der-virt-red}{{A.13}{23}}
\newlabel{v-tc-equiv}{{A.14}{24}}
\newlabel{v-thy-cons-red}{{A.15}{24}}
\newlabel{vd-bt-cons}{{A.16}{24}}
\newlabel{v-bt-cons-equiv}{{A.17}{25}}
\newlabel{v-pres-bt-cons}{{A.17}{25}}
\newlabel{v-fn-bt}{{A.18}{26}}
\newlabel{v-thy-resp}{{A.19}{26}}
\newlabel{v-bt-sm-resp}{{A.20}{26}}
\newlabel{v-bit-con}{{A.21}{26}}
\newlabel{v-subs-not-red-ka}{{A.22}{27}}
\newlabel{v-subst-exists-unique}{{A.23}{27}}
\newlabel{vd-match-rc1}{{A.24}{27}}
\newlabel{vt-match-rc1}{{A.25}{27}}
\newlabel{v-second-sub}{{A.26}{28}}
