proposition: Lemma transport_nsigT : forall {A B} (F : B -> A -> Type) {x y} h z, eq_rect x (fun x => { b : B ⫳ F b x}) z y h = {| dfst := dfst z ; dsnd := eq_rect x (F (dfst z)) (dsnd z) y h |}.
proof: Proof. intros. dependent inversion h. reflexivity. Qed.
imports: Coq.Logic(EqdepFacts)