proposition: Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
proof: Proof. intros A B. destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. - exists f0 g0; trivial. - exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; destruct hf; auto. Qed.