proposition: Lemma Proj1_SPROD_map_law : Map_law (Sprod_l:SPROD -> A).
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