proposition: Lemma ap_fm_cotransitive : (cotransitive ap_fm).
proof: Proof. unfold cotransitive. intro x. induction x. simpl. intro y. case y. intuition. intros c l H z. case z. simpl. intuition. intuition. simpl. intro y. case y. intros H z. case z. intuition. simpl. intuition. intros c l H z. case z. intuition. simpl. intros c0 l0. elim H. clear H. intro H. generalize (ap_cotransitive A a c H c0). intuition. clear H. intro H. generalize (IHx l H l0). intuition. Qed.
imports: CoRN.algebra.CSetoids