Comments 2
Lemma eq_sym_destruct {A} {x y : A} (H : x = y) : y = x.
Proof.
destruct H.
Да, а если в этом примере использовать symmetry in H.
То система их не унифицирует? все еще x = y останется
+1
Sign up to leave a comment.
Lemma eq_sym_destruct {A} {x y : A} (H : x = y) : y = x.
Proof.
destruct H.
Да, а если в этом примере использовать symmetry in H.
То система их не унифицирует? все еще x = y останется
Подробно о Coq: зависимое сопоставление с образцом