proposition: Lemma Equal_Single_equiv : Equivalence Equal_Single.
proof: Proof. unfold Equal_Single in |- *; apply Build_Equivalence; [ trivial | apply Build_Partial_equivalence ]; red in |- *; trivial. Qed.
imports: Setoid BasicTypes