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