proposition: Lemma match_eq_sym_eq : forall T (a b : T) (pf : a = b) F X, match pf in _ = t return F t with | eq_refl => match eq_sym pf in _ = t return F t with | eq_refl => X end end = X.
proof: Proof. destruct pf. reflexivity. Defined.