Mercurial > cpdt > repo

comparison src/MoreDep.v @ 294:1b6c81e51799

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes added while proofreading JFR camera-ready
author Adam Chlipala <adam@chlipala.net>
date Thu, 09 Dec 2010 13:44:57 -0500
parents 2c88fc1dbe33
children 559ec7328410
comparison
equal deleted inserted replaced
293:e2dbc0f1c1e8 294:1b6c81e51799
663 end] ] => dep_destruct T 663 end] ] => dep_destruct T
664 end; crush). 664 end; crush).
665 665
666 (** The balance correctness theorems are simple first-order logic equivalences, where we use the function [projT2] to project the payload of a [sigT] value. *) 666 (** The balance correctness theorems are simple first-order logic equivalences, where we use the function [projT2] to project the payload of a [sigT] value. *)
667 667
668 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) , 668 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
669 present z (projT2 (balance1 a y b)) 669 present z (projT2 (balance1 a y b))
670 <-> rpresent z a \/ z = y \/ present z b. 670 <-> rpresent z a \/ z = y \/ present z b.
671 destruct a; present_balance. 671 destruct a; present_balance.
672 Qed. 672 Qed.
673 673