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