proposition: Lemma InjectsInto_sum X Y X' Y' : InjectsInto X X' -> InjectsInto Y Y' -> InjectsInto (X + Y) (X' + Y').
proof: Proof. intros H1 H2. eapply merely_destruct; try apply H1. intros [f Hf]. eapply merely_destruct; try apply H2. intros [g Hg]. apply tr. exists (fun z => match z with inl x => inl (f x) | inr y => inr (g y) end). intros [x|y] [x'|y'] H. - apply ap. apply Hf. apply path_sum_inl with Y'. apply H. - now apply inl_ne_inr in H. - now apply inr_ne_inl in H. - apply ap. apply Hg. apply path_sum_inr with X'. apply H. 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)