proposition: Lemma AF_irreflexive x: ~(inc x x).
proof: Proof. move => xx; case: (AF (singleton x)); first by apply/nonemptyP; fprops. move => [y /set1_P -> /set0_P s]; case: (s x); apply /setI2_P; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)