proposition: Lemma eq_above_sig {A B} (F : B -> A -> Prop) (G := fun x => sig (fun b => F b x)) {x1 x2 : A} {h : x1 = x2} {z1 : G x1} {z2 : G x2} : proj1_sig z1 = proj1_sig z2 -> z1 =⟨ h ⟩ z2.
proof: Proof. intro Hz. unfold eq_above. unfold G. rewrite (transport_sig F h z1). apply sig_eq. assumption. Qed.
imports: Mon(Base) mathcomp(ssreflect)