proposition: Lemma inv_composeR : forall b, DB b -> f (inv_fun b) = b.
proof: Proof. intros b H; unfold inv_fun,r2i. pattern b, (iota_fun inhA DB DA inv_spec b);eapply iota_fun_ind;eauto. destruct f_b as [H0 H1 H2]. - case (H1 b H); intros x (H',H5); exists x;auto. repeat split; trivial. intros x' [H3 H4]; subst b ; apply H2; auto. now destruct H3 as [_ [H3 H5]]. - destruct 1 as [[H0 _] _]; destruct H0; tauto. Qed.
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)