proposition: Lemma Equal_SubType_equiv : Equivalence Equal_SubType.
proof: Proof. apply Build_Equivalence. unfold Reflexive in |- *; intro x; exact (Refl (Elt_sub x)). apply Build_Partial_equivalence. unfold Transitive in |- *; intros a b c H1 H2; unfold Equal_SubType in |- *. apply Trans with (Elt_sub b); auto. unfold Symmetric in |- *; intros a b H; unfold Equal_SubType in |- *. apply Sym; auto. Qed.
imports: Map