-theorem true_to_pi_p_Sn:
-\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
-p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).
+(*
+notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π)
+ )
+ \below
+ (p
+ \atop
+ (ident i < n)) f"
+non associative with precedence 60 for
+@{ 'product $n (λ${ident i}:$xx1.$p) (λ${ident i}:$xx2.$f) }.
+
+notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π)
+ )
+ \below
+ ((ident i < n)) f"
+non associative with precedence 60 for
+@{ '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"
+non associative with precedence 60
+for @{ 'product $n (λ${ident x}.$p) (λ${ident x}.$f) }.
+
+notation > "'Pi' (ident x) ≤ n | p . term 46 f"
+non associative with precedence 60
+for @{ 'product (S $n) (λ${ident x}.$p) (λ${ident x}.$f) }.
+
+notation > "'Pi' (ident x) < n . term 46 f"
+non associative with precedence 60
+for @{ 'product $n (λ_.true) (λ${ident x}.$f) }.
+*)
+
+theorem true_to_pi_p_Sn: ∀n,p,g.
+ p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).