proposition: Lemma sym_apfun : forall A B : CSetoid, Csymmetric (ap_fun A B).
proof: Proof. unfold Csymmetric in |- *. unfold ap_fun in |- *. intros A B f g H. elim H. clear H. intros a H. exists a. apply ap_symmetric. exact H. Qed.
imports: CoRN.algebra.CSetoids