Подробно о Coq: зависимое сопоставление с образцом

[Natasha_Klaus]

Lemma eq_sym_destruct {A} {x y : A} (H : x = y) : y = x.

Proof.

destruct H.

Да, а если в этом примере использовать symmetry in H.

То система их не унифицирует? все еще x = y останется

[andreykl]

Унифицирует :) . Можно и в режиме написания кода eq_sym использовать в подобном случае (там дальше примеры есть в статье).