X Y : infinite X -> Injection X Y -> infinite Y. Proof. apply Injection_trans. Qed.
From HoTT Require Import Basics Types TruncType. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card Spaces.Nat.Core.