proposition: Lemma inv_fun_bij : fun_bijection DB DA inv_fun.
proof: Proof. destruct f_b; split. - intros b Hb; unfold inv_fun, r2i. pattern b, (iota_fun inhA DB DA inv_spec b); eapply iota_fun_ind;eauto. + destruct (H0 b Hb) as [x H2]. exists x;split ;auto. unfold inv_spec; repeat split; auto. 1,2,3 : tauto. destruct 1. apply H1; auto. tauto. destruct H3 as [H3 H5]. destruct H2, H5; congruence. + destruct 1; tauto. - intros a Ha; exists (f a);split;auto. apply inv_compose;auto. - intros b b' Hb Hb' H2. rewrite <- (inv_composeR Hb). rewrite <- (inv_composeR Hb'). now rewrite H2. Qed.
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)