Réécriture au niveau du type

Question

je l'Etat preuve suivante:

1 subgoals 
U : Type 
X : Ensemble U 
Y : Ensemble U 
f : U -> U 
g : U -> U 
pF : proof_dom_cod U X Y f 
pG : proof_dom_cod U X Y g 
fg : f = g 
H : proof_dom_cod U X Y g = proof_dom_cod U X Y f 
______________________________________(1/1) 
createarrow U X Y f pF = createarrow U X Y g pG 

Je veux

assert (pF = pG) 

et ensuite utiliser la non-pertinence preuve pour prouver que. Malheureusement, pF = pG n'est pas valide car ils ont des types différents, même si je sais que les types sont les mêmes, car H. dire rewrite H ou rewrite H in pF conduit à un échec de correspondance, je suppose que in pF se réfère à la valeur pas le type.

Existe-t-il un équivalent à rewrite pour les types?

Voici le théorème que j'essaie de compléter (avec toutes les définitions nécessaires).

Require Import Coq.Logic.FunctionalExtensionality. 
Require Import Coq.Sets.Ensembles. 
Require Import Coq.Logic.Classical_Prop. 


Definition proof_dom_cod 
(U : Type) (X Y : Ensemble U) (f : U -> U) : Prop 
    := forall x : U, In U X x -> In U Y (f x). 

Inductive setarrow (U : Type) (X Y : Ensemble U) : Type 
     := 
    | createarrow (f : U -> U) (proof : proof_dom_cod U X Y f). 

Lemma eq_setarrow 
    (U : Type) (X Y : Ensemble U) (f g : U -> U) (pF : proof_dom_cod U X Y f) (pG : proof_dom_cod U X Y g) 
     : (f = g -> (createarrow U X Y f pF = createarrow U X Y g pG)). 
    intros fg. 
    assert (proof_dom_cod U X Y g = proof_dom_cod U X Y f). 
     rewrite fg. 
     trivial. 
Qed. 

Answer 1

Ce n'est pas une réponse à la question générale, mais ici subst fait le travail. La preuve peut être finie comme suit:

subst f. 
apply f_equal. apply proof_irrelevance.