proposition: Lemma Proj2_SPROD_map_law : Map_law (Sprod_r:SPROD -> B).
proof: Proof. unfold Map_law in |- *; simpl in |- *. simple induction x; intros a b; simple induction y; intros a' b'. simpl in |- *; unfold Equal_Sprod in |- *; simpl in |- *. simple induction 1; trivial. Qed.
imports: Map