proposition: Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B).
proof: Proof. intros A B. unfold irreflexive in |- *. intros f. unfold ap_fun in |- *. red in |- *. intro H. elim H. intros a H0. set (H1 := ap_irreflexive B (f a)) in *. intuition. Qed.
imports: CoRN.algebra.CSetoids