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: Relations