proposition: Lemma ap_fm_irreflexive: (irreflexive ap_fm).
proof: Proof. unfold irreflexive. intro x. induction x. simpl. red. intuition. simpl. red. intro H. apply IHx. elim H. clear H. generalize (ap_irreflexive A a). unfold Not. intuition. intuition. Qed.
imports: CoRN.algebra.CSetoids