include "Universes.ma".

nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
{ first: A;
  second: B
}.

interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r).
interpretation "Cartesian" 'product A B = (Cartesian A B).

notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
 with precedence 10
for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }.