proposition: Lemma transport_subtype : forall {A B} (F : B -> A -> Prop) {x y} h z, eq_rect x (fun x => subtype (fun b => F b x)) z y h = {| wit := wit z ; pf := eq_ind x (F (wit z)) (pf z) y h |}.
proof: Proof. intros. dependent inversion h. reflexivity. Qed.
imports: Coq.Logic(EqdepFacts)