proposition: Lemma identity_bijective : forall x, Transformation.bijective x x (fun y => y).
proof: Proof. ir. uhg; dj. ap Transformation.identity_axioms. uhg; ee. am. uhg; ir. sh x0. ee. am. tv. uhg; ee; try am. uhg; ir. am. Qed.
imports: set_theory