proposition: Lemma id_hsubtype_preserving {X : UU} (U : hsubtype X) : hsubtype_preserving U U (idfun X).
proof: Proof. intros x xinU. rewrite image_hsubtype_id in xinU. exact xinU. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions