Umschreiben auf der Typebene

Question

Ich habe den folgenden Beweis Zustand:

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 

Deshalb möchte ich

assert (pF = pG) 

und dann Beweis Irrelevanz verwenden, das zu beweisen. Leider ist pF = pG nicht gültig, weil sie verschiedene Typen haben, obwohl ich die Typen kenne, die gleich sind, weil H. sagen rewrite H oder rewrite H in pF führt zu einem Match-Fehler, ich nehme an, weil in pF bezieht sich auf den Wert nicht der Typ.

Gibt es ein Äquivalent zu rewrite für Typen?

Hier ist der Satz, den ich versuche zu vervollständigen (mit allen notwendigen Definitionen). Diese

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

ist keine Antwort auf die allgemeine Frage, aber hier subst macht die Arbeit. Der Beweis kann wie folgt abgeschlossen werden:

subst f. 
apply f_equal. apply proof_irrelevance.