proposition: Lemma sigT_rewrite_2:forall (X Y Z:Set) (P:(X->Z->Prop)) (h1:Y=Z), let id_lft:=(fun y:Y=>(eq_rec Y (fun Z0 : Set => Z0) y Z h1)) in {f:X->Y | forall x, P x (id_lft (f x))} -> {g:X->Z | forall x, P x (g x)}.
proof: Proof. intros X Y Z P h1 id_lft [f hyp_f]. set (id_rht:=(fun z:Z => eq_rec Y (fun Z0 : Set => Z0 -> Y) (fun y0 : Y => y0) Z h1 z):Z->Y). exists (fun x=> id_lft (f x)). assumption. Defined.
imports: ExtensionalFunctor Setoid