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