proposition: Lemma inv_compose : forall x, DA x -> inv_fun (f x) = x.
proof: Proof. intros x H; unfold inv_fun, r2i. pattern (f x), (iota_fun inhA DB DA inv_spec (f x)). eapply (iota_fun_ind inhA DB DA). - destruct f_b; now apply H0. - reflexivity. - exists x; split. + split. * destruct f_b; split;auto. * auto. + intros x' H0; destruct f_b as [f0 f1 f2]. apply f2; auto. now destruct H0. now destruct H0 as [[H0 [_ H2]] H1]. - destruct f_b as [f0 f1 f2]. apply f0;auto. - intros b H0; destruct H0 as [H0 H1]; apply H1; auto. split;auto. split;auto. split;auto; now apply f_b. Qed.
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)