fact: Variables (A B : Type) (Ha : inhabited A) (Hb:inhabited B) (DA: Ensemble A) (DB : Ensemble B).
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)