proposition: Lemma noid_inl_prop7 (A := inductive_limit noid_ind_system) (B:= noid_limit): bijection_prop (Lf noid_can A B) A B.
proof: Proof. move:noid_inl_equiv_esr => [Er Sr]. saw; apply: lf_bijective. - move => x /inductive_limit_hi /= [ha hb hc]. apply:inc_class_setQ; rewrite (proj2 noid_inl_equiv_esr). by apply/noid_inl_sumP; aw; split; fprops;apply:noid_prop5a. - move => u v /inductive_limit_hi /= [ha hb hc] /inductive_limit_hi /= [ha' hb' hc']. rewrite {2} hc {2} hc' /noid_can. by move/(noid_inl_class_compat ha ha' hb hb'). - move => y /(setQ_P Er)[]; rewrite Sr; move/noid_inl_sumP. set i := Q _; set z := P _; move => [pry iI zE] yv. move: (noid_inl_class_ii iI zE)=> [qa qb qc qd]. rewrite yv - pry qd /noid_can. set t := (Vf (Vg f (J i i)) z). set c := (class (inl_equiv noid_ind_system) (J t i)). have cA: inc c A by apply: inl_class_in_lim. move/inductive_limit_hi: (cA) => /= [ra rb rc]. by ex_tac; apply/(noid_inl_class_compat iI ra qa rb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)