proposition: Lemma ap_fm_symmetric: Csymmetric ap_fm.
proof: Proof. unfold Csymmetric. intros x. induction x. intro y. case y. simpl. intuition. simpl. intuition. simpl. intro y. case y. simpl. intuition. simpl. intros c l H0. elim H0. generalize (ap_symmetric A a c). intuition. clear H0. intro H0. right. apply IHx. exact H0. Qed.
imports: CoRN.algebra.CSetoids