proposition: Lemma eq_sym_eq : forall T (a b : T) (pf : a = b) (F : T -> Type) val, match eq_sym pf in _ = x return F x with | eq_refl => val end = match pf in _ = x return F x -> F a with | eq_refl => fun x => x end val.
proof: Proof. destruct pf. reflexivity. Defined.