proposition: Lemma IFE_consec_chain2 x : inc x IFSE -> exists2 f, inc f (consec_lists_for IFS_order x) & domain f = IFS_pow x.
proof: Proof. move => xE. move: (IFE_consec_chain xE) => hyp. exists (IFS_chain x); first by apply/consec_pow_pr0. by rewrite /IFS_chain; aw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)