Mercurial > cpdt > repo

comparison src/LogicProg.v @ 445:0650420c127b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finished vertical spacing
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Aug 2012 17:31:56 -0400
parents 8077352044b2
children 9fbf3b4dac29
comparison
equal deleted inserted replaced
444:0d66f1a710b8 445:0650420c127b
944 Hint Rewrite f_g. 944 Hint Rewrite f_g.
945 945
946 Lemma f_f_f' : forall x, f (f (f x)) = f x. 946 Lemma f_f_f' : forall x, f (f (f x)) = f x.
947 intros; autorewrite with core. 947 intros; autorewrite with core.
948 (** [[ 948 (** [[
949
950 ============================ 949 ============================
951 g (g (g x)) = g x 950 g (g (g x)) = g x
952 951
953 subgoal 2 is: 952 subgoal 2 is:
954 P x 953 P x