proposition: Lemma cotrans_apfun : forall A B : CSetoid, cotransitive (ap_fun A B).
proof: Proof. intros A B. unfold cotransitive in |- *. unfold ap_fun in |- *. intros f g H h. elim H. clear H. intros a H. set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *. elim H1. clear H1. intros H1. left. exists a. exact H1. clear H1. intro H1. right. exists a. exact H1. Qed.
imports: CoRN.algebra.CSetoids