proposition: Lemma inverse_map_ens_sym {A B : Type} (f : A -> B) (g : B -> A) U V : inverse_map_ens f g U V -> inverse_map_ens g f V U.
proof: Proof. firstorder. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)