Unfold [transitivity] and [symmetry] in the corresponding tactics

It's not possible to write `let (R,x,y) := match goal ... end in`?