On the degeneracy of sigma-types in presence of computational classical logic
-----------------------------------------------------------------------------
                             (erratum)

In sections 2.1 and 2.4, "subst pi pi" is missing in the grammar for pi.

The completed syntax in section 2.1 is

t,u ::= x | wit pi
pi  ::= (t,pi) | prf pi | refl | subst pi pi

The completed syntax in section 2.4 is

t,u ::= x | wit pi | cc_k^x.A t
pi  ::= (t,pi) | prf pi | refl | subst pi pi
     | cc_{k:neg A} pi | th_B k pi | th_B k t