Entry tags:
жалоба
Coq. Теоремы. Затрахался. Идет как зуб мудрости. Каждая. В этой главе еще 300 с лишним строк примеров.
Entry tags:
coq
Took me some time to prove
But I did.
Theorem distr_rev : forall l1 l2 : natlist, rev (l1 ++ l2) = (rev l2) ++ (rev l1).
But I did.
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif){kind=small}