proposition: Lemma transport_sig : forall {A B} (F : B -> A -> Prop) {x y} h z, eq_rect x (fun x => sig (fun b => F b x)) z y h = exist _ (proj1_sig z) (@eq_ind A x (F (proj1_sig z)) (proj2_sig z) y h).
proof: Proof. intros. dependent inversion h. compute. destruct z. reflexivity. Qed.
imports: Mon(Base) mathcomp(ssreflect)