take I --> pcs-empty ; :: thesis: I --> pcs-empty is ()
thus I --> pcs-empty is () ; :: thesis: verum