proposition: Lemma AF_infinite_seq x: well_founded_set x.
proof: Proof. move => f ff sf hf. case: (AF (Imf f)). move => ie; empty_tac1 (Vf f \0c); apply/(Imf_P ff). rewrite sf; exists \0c => //; apply:NS0. move => [y /(Imf_P ff) [u usf -> h]]; rewrite sf in usf. case: (in_set0 (x := Vf f (csucc u))). rewrite -h. empty_tac1 (Vf f (csucc u)). by apply/(Imf_P ff); exists (csucc u) => //; rewrite sf;apply:NS_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)