proposition: Lemma PathOverUniqueness {X:Type} {x x':X} (p:x=x') {Y : X -> Type} (y : Y x) : ∃! (y' : Y x'), PathOver p y y'.
proof: Proof. induction p. apply iscontrcoconusfromt. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA