@{ 'product $n (λ_:$xx1.$xx3) (λ${ident i}:$xx2.$f) }.
interpretation "big product" 'product n p f = (pi_p n p f).
notation > "'Pi' (ident x) < n | p . term 46 f"
@{ 'product $n (λ_:$xx1.$xx3) (λ${ident i}:$xx2.$f) }.
interpretation "big product" 'product n p f = (pi_p n p f).
notation > "'Pi' (ident x) < n | p . term 46 f"