coq | dmytrish

dmytrish

destruct them all

dmytrish Jun 30, 2014 00:18

Є, значить, тут теоремка із першого розділу Software Foundations:

Theorem andb_eq_orb:
forall (b c : bool), (andb b c = orb b c) -> b = c.

( малозв’язні спроби довести >>> )

програмістське, coq, fp

Leave a comment 9