proposition: Lemma match_eq_match_eq : forall T F (a b : T) (pf : a = b) X Y, X = Y -> match pf in _ = T return F T with | eq_refl => X end = match pf in _ = T return F T with | eq_refl => Y end.
proof: Proof. intros. subst. auto. Defined.