proposition: Lemma inductive_limit_Iv S S': inl_same_data S S' -> inductive_limit S = inductive_limit S'.
proof: Proof. by move / inl_equiv_Iv;rewrite /inductive_limit => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)