proposition: Lemma hereditarily_finite_pr x: hereditarily_finite x -> finite_set x /\ (forall y, inc y x -> hereditarily_finite y).
proof: Proof. move=> [pa [m mN xe]]. move: (rept_union_pr x) => [sa sb]. split; first by move: (pa _ NS0); rewrite sa. move => y /rept_union_inc aux. split. move => n nN; exact (sub_finite_set (aux _ nN) (pa _ (NS_succ nN))). exists m; first by exact. by move: (aux _ mN); rewrite (sb _ mN) xe setU_0 => /sub_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)