proposition: Lemma InjectsInto_power_morph X Y : InjectsInto X Y -> InjectsInto (X -> HProp) (Y -> HProp).
proof: Proof. intros HF. eapply merely_destruct; try apply HF. intros [f Hf]. apply tr. exists (fun p => fun y => hexists (fun x => p x /\ y = f x)). intros p q H. apply path_forall. intros x. apply equiv_path_iff_hprop. split; intros Hx. - assert (Hp : (fun y : Y => hexists (fun x : X => p x * (y = f x))) (f x)). { apply tr. exists x. split; trivial. } pattern (f x) in Hp. rewrite H in Hp. eapply merely_destruct; try apply Hp. now intros [x'[Hq <- % Hf]]. - assert (Hq : (fun y : Y => hexists (fun x : X => q x * (y = f x))) (f x)). { apply tr. exists x. split; trivial. } pattern (f x) in Hq. rewrite <- H in Hq. eapply merely_destruct; try apply Hq. now intros [x'[Hp <- % Hf]]. Qed.
imports: HoTT(TruncType ExcludedMiddle abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card) HoTT(Equiv.BiInv) HoTT(HIT.unique_choice) HoTT.Sets(Ordinals Hartogs Powers GCH AC)