proposition: Lemma Ext_equiv : Equivalence Ext.
proof: Proof. intros; apply Build_Equivalence. unfold Reflexive in |- *; unfold Ext in |- *; intros f x. apply Refl. apply Build_Partial_equivalence. unfold Transitive in |- *; unfold Ext in |- *; intros f g h e1 e2 x. apply Trans with (g x). apply (e1 x). apply (e2 x). unfold Symmetric in |- *; unfold Ext in |- *; intros f g e x. apply Sym; trivial. Qed.
imports: Setoid