-interpretation "exT2 \fst" 'pi1 = (pi1exT23 _ _ _ _).
-interpretation "exT2 \fst" 'pi1a x = (pi1exT23 _ _ _ _ x).
-interpretation "exT2 \fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y).
+interpretation "exT2 \fst" 'pi1 = (pi1exT23 ? ? ? ?).
+interpretation "exT2 \fst" 'pi1a x = (pi1exT23 ? ? ? ? x).
+interpretation "exT2 \fst" 'pi1b x y = (pi1exT23 ? ? ? ? x y).