proposition: Lemma isinj_embedding_beta {X Y : Type} (f : X -> Y) {I : IsEmbedding f} {x : X} : (isinj_embedding f I x x idpath) = idpath.
proof: Proof. exact (ap (ap pr1) (contr (idpath : (x;idpath) = (x;idpath)))). Defined.
imports: Basics Types.Sigma Types.Forall Types.Paths Types.Unit Types.Arrow