proposition: Lemma ta_apfun : forall A B : CSetoid, tight_apart (eq_fun A B) (ap_fun A B).
proof: Proof. unfold tight_apart in |- *. unfold ap_fun in |- *. unfold eq_fun in |- *. intros A B f g. split. intros H a. red in H. apply not_ap_imp_eq. red in |- *. intros H0. apply H. exists a. exact H0. intros H. red in |- *. intro H1. elim H1. intros a X. set (H2 := eq_imp_not_ap B (f a) (g a) (H a) X) in *. exact H2. Qed.
imports: CoRN.algebra.CSetoids