proposition: Lemma eq_above_subtype {A B} (f : A -> B) (HB : UIP_ B) (G := fun y => {x : A ∥ f x = y}) {y1 y2 : B} {h : y1 = y2} {z1 : G y1} {z2 : G y2} : z1.(wit) = z2.(wit) -> z1 =⟨ h ⟩ z2.
proof: Proof. intro Hz. unfold eq_above. unfold G in *. rewrite (transport_subtype _ h z1). eapply (eq_eq_above_eq_subtype _ _ _ _). Unshelve. 2: simpl ; assumption. apply HB. Qed.
imports: Coq.Logic(EqdepFacts)