- 1
- 2
- 3
- 4
- 5
- 6
Lemma use_prop_equality : forall {X} (f : X -> Prop) a b,
a = b -> f a -> f b.
Proof.
intros X f a b He Ha.
destruct He. apply Ha.
Qed.
Нашли или выдавили из себя код, который нельзя назвать нормальным, на который без улыбки не взглянешь? Не торопитесь его удалять или рефакторить, — запостите его на говнокод.ру, посмеёмся вместе!
+2
Lemma use_prop_equality : forall {X} (f : X -> Prop) a b,
a = b -> f a -> f b.
Proof.
intros X f a b He Ha.
destruct He. apply Ha.
Qed.
Тактика rewrite не нужна.
К слову, вот более полезная лемма
@CHayT, ты используешь шрифт с лигатурами?
Умляуты тоже занятные: они произошли от дифтонгов ae, oe, ue, в которых e постепенно уехал вверх букв. В средневековых шрифтах e выглядела очень похоже на n, и в итоге стала двумя чёрточками. Форма с e полностью эквивалентна форме с умляутами и встречается довольно часто (например, при использовании анскильного шрифта без умляутов).
В Германии практически не встречаются слова, в которых e следует за буквой с умляутом (потому что если раскрыть умляют, будет две e подряд, некрасиво, это как о писать после ё). А вот в Швейцарии таких полно, например, в именах собственных: Üetliberg, к примеру. Когда их пишут без умляутов, дополнительную е вроде бы не добавляют.
Или я плохо искал?
Это тоже дифтонг, он соответствует в точности тому же звуку, что и -eu- и произносится как "ой". Он обычно появляется при склонении слов, которые содержат -au- (e.g. laufen -> läuft).
То, что гласные рядом с умляутами не стоят – это логично, сложно же такое произносить.
https://de.wiktionary.org/wiki/Koeffizient
Произнося это слово, немец должен споткнуться два раза.
Не более, чем в русском. "Baum" звучит практически так же, как "баум".
> заморский «тротуар»
В немецком тоже есть куча исключений в произношении заимствованных слов (Portemonnaie)
В русском «ау» образует два слога, в немецком «au» образует один слог. Это важно для стихотворений.
> В немецком тоже есть куча исключений
Особенно неприятно, когда в одном предложении встречается английское Sweatshirt и французское Portemonnaie. Приходится ломать парсер на каждом слове.