proposition: Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B) (y : {y:A | y = x}), match_eq A B x fn = fn y.
proof: Proof. intros A B x fn y. unfold match_eq. f_equal. destruct y. apply <- subset_eq. symmetry. assumption. Qed.
imports: Coq.Program.Utils Coq.Program.Equality ProofIrrelevance