Using Coq, prove by induction that (C B0) (C B1) . . .(C Bn) = C (B0 B1 . . . Bn)

Template:

Require Import Ensembles. 

Variable B : nat -> (Ensemble U). Fixpoint unionB (n : nat) : Ensemble U := match n with | 0 => B 0 | S m => Union U (unionB m) (B (S m)) end. Fixpoint intersectionCB (n : nat) : Ensemble U := match n with | 0 => Setminus U C (B 0) | S m => Intersection U (intersectionCB m) (Setminus U C (B (S m))) end. Theorem generalizedIntersectionSetminusAlt : forall n : nat, intersectionCB n = Setminus U C (unionB n). Proof. induction n. apply Extensionality_Ensembles. (* to be completed *) Qed.