+(* distributivity *)
+
+record Dop (A:Type[0]) (nil:A): Type[0] ≝
+ {sum : ACop A nil;
+ prod: A → A →A;
+ null: \forall a. prod a nil = nil;
+ distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
+ }.
+
+theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.\forall f,a.
+ let aop \def sum B nil R in
+ let mop \def prod B nil R in
+ mop a \big[aop,nil]_{i<n|p i}(f i) =
+ \big[aop,nil]_{i<n|p i}(mop a (f i)).
+#n #p #B #nil #R #f #a normalize (elim n) [@null]
+#n #Hind (cases (true_or_false (p n))) #H
+ [>bigop_Strue // >bigop_Strue // >(distr B nil R) >Hind //
+ |>bigop_Sfalse // >bigop_Sfalse //
+ ]
+qed.
+
+(* Sigma e Pi
+
+