proposition: Lemma eq_above_nsigT_hprop {A B} (f : A -> B -> Type) (hprop_f : forall x y (p q : f x y), p = q) (G := fun y => {x : A ⫳ f x y}) {y1 y2 : B} {h : y1 = y2} {z1 : G y1} {z2 : G y2} : dfst z1 = dfst z2 -> z1 =⟨ h ⟩ z2.
proof: Proof. intro Hz. unfold eq_above. unfold G in *. rewrite (transport_nsigT _ h z1). eapply (eq_eq_above_eq_nsigT _ _ _ _). Unshelve. 2: simpl ; assumption. apply hprop_f. Qed.
imports: Coq.Logic(EqdepFacts)