proposition: Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B) `{!Inj (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
proof: Proof. intros. apply submseteq_length_Permutation. - by apply finite_inj_submseteq. - rewrite fmap_length. by apply Nat.eq_le_incl. Qed.
imports: stdpp(options)