-interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).
-
-coinductive product (A,B:Type) : Type ≝ pair : ∀a:A.∀b:B.product A B.
-
-notation "a \times b" left associative with precedence 70 for @{'product $a $b}.
-interpretation "prod" 'product a b = (product a b).
-
-definition first : ∀A.∀P.A × P → A ≝ λA,P,s.match s with [pair x _ ⇒ x].
-definition second : ∀A.∀P.A × P → P ≝ λA,P,s.match s with [pair _ y ⇒ y].
-
-interpretation "pair pi1" 'pi1 = (first _ _).
-interpretation "pair pi2" 'pi2 = (second _ _).
-interpretation "pair pi1" 'pi1a x = (first _ _ x).
-interpretation "pair pi2" 'pi2a x = (second _ _ x).
-interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
-interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
-
-notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}.
-interpretation "pair" 'pair a b = (pair _ _ a b).