proposition: Lemma Dl2_map_eq : forall (f1 : DP1 -c> DP1) (f2:DP2 -c> DP2) (d:Dprodi DI2), DI2_map f1 f2 d == pair2 (f1 (pi1 d)) (f2 (pi2 d)).
proof: Proof. intros; simpl; apply Oprodi_eq_intro; intro b; case b; trivial. Qed.