proposition: Lemma Equal_Sprod_equiv : Equivalence Equal_Sprod.
proof: Proof. apply Build_Equivalence. unfold Reflexive in |- *; simple induction x; intros a b; unfold Equal_Sprod in |- *; simpl in |- *. split. apply Refl. apply Refl. apply Build_Partial_equivalence. unfold Transitive in |- *. simple induction x; intros a b; simple induction y; intros a' b'; simple induction z; intros a'' b''. unfold Equal_Sprod in |- *; simpl in |- *. intros H H0; elim H; intros H1 H2; elim H0; intros H3 H4. split. apply Trans with a'; trivial. apply Trans with b'; trivial. unfold Symmetric in |- *; simple induction x; intros a b; simple induction y; intros a' b'. unfold Equal_Sprod in |- *; simpl in |- *. intros H; elim H; intros H1 H2. split. apply Sym; trivial. apply Sym; trivial. Qed.
imports: Map