helm/software/matita/contribs/procedural/CoRN/algebra/CSetoidFun.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: CSetoidFun.v,v 1.10 2004/04/23 10:00:53 lcf Exp $ *)
  20
  21 include "algebra/CSetoids.ma".
  22
  23 (* UNEXPORTED
  24 Section unary_function_composition
  25 *)
  26
  27 (*#* ** Composition of Setoid functions
  28
  29 Let [S1],  [S2] and [S3] be setoids, [f] a
  30 setoid function from [S1] to [S2], and [g] from [S2]
  31 to [S3] in the following definition of composition.  *)
  32
  33 (* UNEXPORTED
  34 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S1.var
  35 *)
  36
  37 (* UNEXPORTED
  38 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S2.var
  39 *)
  40
  41 (* UNEXPORTED
  42 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S3.var
  43 *)
  44
  45 (* UNEXPORTED
  46 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/f.var
  47 *)
  48
  49 (* UNEXPORTED
  50 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/g.var
  51 *)
  52
  53 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_fun.con" as definition.
  54
  55 (* UNEXPORTED
  56 End unary_function_composition
  57 *)
  58
  59 (* UNEXPORTED
  60 Section unary_and_binary_function_composition
  61 *)
  62
  63 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_un_fun.con" as definition.
  64
  65 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_fun.con" as definition.
  66
  67 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_un_bin_fun.con" as definition.
  68
  69 (* UNEXPORTED
  70 End unary_and_binary_function_composition
  71 *)
  72
  73 (*#* ***Projections
  74 *)
  75
  76 (* UNEXPORTED
  77 Section function_projection
  78 *)
  79
  80 inline procedural "cic:/CoRN/algebra/CSetoidFun/proj_bin_fun.con" as lemma.
  81
  82 inline procedural "cic:/CoRN/algebra/CSetoidFun/projected_bin_fun.con" as definition.
  83
  84 (* UNEXPORTED
  85 End function_projection
  86 *)
  87
  88 (* UNEXPORTED
  89 Section BinProj
  90 *)
  91
  92 (* UNEXPORTED
  93 cic:/CoRN/algebra/CSetoidFun/BinProj/S.var
  94 *)
  95
  96 inline procedural "cic:/CoRN/algebra/CSetoidFun/binproj1.con" as definition.
  97
  98 inline procedural "cic:/CoRN/algebra/CSetoidFun/binproj1_strext.con" as lemma.
  99
 100 inline procedural "cic:/CoRN/algebra/CSetoidFun/cs_binproj1.con" as definition.
 101
 102 (* UNEXPORTED
 103 End BinProj
 104 *)
 105
 106 (*#* **Combining operations
 107 %\begin{convention}% Let [S1], [S2] and [S3] be setoids.
 108 %\end{convention}%
 109 *)
 110
 111 (* UNEXPORTED
 112 Section CombiningOperations
 113 *)
 114
 115 (* UNEXPORTED
 116 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S1.var
 117 *)
 118
 119 (* UNEXPORTED
 120 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S2.var
 121 *)
 122
 123 (* UNEXPORTED
 124 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S3.var
 125 *)
 126
 127 (*#*
 128 In the following definition, we assume [f] is a setoid function from
 129 [S1] to [S2], and [op] is an unary operation on [S2].
 130 Then [opOnFun] is the composition [op] after [f].
 131 *)
 132
 133 (* UNEXPORTED
 134 Section CombiningUnaryOperations
 135 *)
 136
 137 (* UNEXPORTED
 138 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/f.var
 139 *)
 140
 141 (* UNEXPORTED
 142 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/op.var
 143 *)
 144
 145 inline procedural "cic:/CoRN/algebra/CSetoidFun/opOnFun.con" as definition.
 146
 147 (* UNEXPORTED
 148 End CombiningUnaryOperations
 149 *)
 150
 151 (* UNEXPORTED
 152 End CombiningOperations
 153 *)
 154
 155 (*#* **Partial Functions
 156
 157 In this section we define a concept of partial function for an
 158 arbitrary setoid.  Essentially, a partial function is what would be
 159 expected---a predicate on the setoid in question and a total function
 160 from the set of points satisfying that predicate to the setoid.  There
 161 is one important limitations to this approach: first, the record we
 162 obtain has type [Type], meaning that we can't use, for instance,
 163 elimination of existential quantifiers.
 164
 165 Furthermore, for reasons we will explain ahead, partial functions will
 166 not be defined via the [CSetoid_fun] record, but the whole structure
 167 will be incorporated in a new record.
 168
 169 Finally, notice that to be completely general the domains of the
 170 functions have to be characterized by a [CProp]-valued predicate;
 171 otherwise, the use you can make of a function will be %\emph{%#<i>#a
 172 priori#</i>#%}% restricted at the moment it is defined.
 173
 174 Before we state our definitions we need to do some work on domains.
 175 *)
 176
 177 (* UNEXPORTED
 178 Section SubSets_of_G
 179 *)
 180
 181 (*#* ***Subsets of Setoids
 182
 183 Subsets of a setoid will be identified with predicates from the
 184 carrier set of the setoid into [CProp].  At this stage, we do not make
 185 any assumptions about these predicates.
 186
 187 We will begin by defining elementary operations on predicates, along
 188 with their basic properties.  In particular, we will work with well
 189 defined predicates, so we will prove that these operations preserve
 190 welldefinedness.
 191
 192 %\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp].
 193 %\end{convention}%
 194 *)
 195
 196 (* UNEXPORTED
 197 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/S.var
 198 *)
 199
 200 (* UNEXPORTED
 201 Section Conjunction
 202 *)
 203
 204 (* UNEXPORTED
 205 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/P.var
 206 *)
 207
 208 (* UNEXPORTED
 209 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/Q.var
 210 *)
 211
 212 inline procedural "cic:/CoRN/algebra/CSetoidFun/conjP.con" as definition.
 213
 214 inline procedural "cic:/CoRN/algebra/CSetoidFun/prj1.con" as lemma.
 215
 216 inline procedural "cic:/CoRN/algebra/CSetoidFun/prj2.con" as lemma.
 217
 218 inline procedural "cic:/CoRN/algebra/CSetoidFun/conj_wd.con" as lemma.
 219
 220 (* UNEXPORTED
 221 End Conjunction
 222 *)
 223
 224 (* UNEXPORTED
 225 Section Disjunction
 226 *)
 227
 228 (* UNEXPORTED
 229 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/P.var
 230 *)
 231
 232 (* UNEXPORTED
 233 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/Q.var
 234 *)
 235
 236 (*#*
 237 Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
 238 *)
 239
 240 inline procedural "cic:/CoRN/algebra/CSetoidFun/disj.con" as definition.
 241
 242 inline procedural "cic:/CoRN/algebra/CSetoidFun/inj1.con" as lemma.
 243
 244 inline procedural "cic:/CoRN/algebra/CSetoidFun/inj2.con" as lemma.
 245
 246 inline procedural "cic:/CoRN/algebra/CSetoidFun/disj_wd.con" as lemma.
 247
 248 (* UNEXPORTED
 249 End Disjunction
 250 *)
 251
 252 (* UNEXPORTED
 253 Section Extension
 254 *)
 255
 256 (*#*
 257 The next definition is a bit tricky, and is useful for choosing among the elements that satisfy a predicate [P] those that also satisfy [R] in the case where [R] is only defined for elements satisfying [P]---consider [R] to be a condition on the image of an object via a function with domain [P].  We chose to call this operation [extension].
 258 *)
 259
 260 (* UNEXPORTED
 261 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/P.var
 262 *)
 263
 264 (* UNEXPORTED
 265 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/R.var
 266 *)
 267
 268 inline procedural "cic:/CoRN/algebra/CSetoidFun/extend.con" as definition.
 269
 270 inline procedural "cic:/CoRN/algebra/CSetoidFun/ext1.con" as lemma.
 271
 272 inline procedural "cic:/CoRN/algebra/CSetoidFun/ext2_a.con" as lemma.
 273
 274 inline procedural "cic:/CoRN/algebra/CSetoidFun/ext2.con" as lemma.
 275
 276 inline procedural "cic:/CoRN/algebra/CSetoidFun/extension_wd.con" as lemma.
 277
 278 (* UNEXPORTED
 279 End Extension
 280 *)
 281
 282 (* UNEXPORTED
 283 End SubSets_of_G
 284 *)
 285
 286 (* NOTATION
 287 Notation Conj := (conjP _).
 288 *)
 289
 290 (* UNEXPORTED
 291 Implicit Arguments disj [S].
 292 *)
 293
 294 (* UNEXPORTED
 295 Implicit Arguments extend [S].
 296 *)
 297
 298 (* UNEXPORTED
 299 Implicit Arguments ext1 [S P R x].
 300 *)
 301
 302 (* UNEXPORTED
 303 Implicit Arguments ext2 [S P R x].
 304 *)
 305
 306 (*#* ***Operations
 307
 308 We are now ready to define the concept of partial function between arbitrary setoids.
 309 *)
 310
 311 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind".
 312
 313 (* COERCION
 314 cic:/matita/CoRN-Procedural/algebra/CSetoidFun/bpfpfun.con
 315 *)
 316
 317 (* NOTATION
 318 Notation BDom := (bpfdom _ _).
 319 *)
 320
 321 (* UNEXPORTED
 322 Implicit Arguments bpfpfun [S1 S2].
 323 *)
 324
 325 (*#*
 326 The next lemma states that every partial function is well defined.
 327 *)
 328
 329 inline procedural "cic:/CoRN/algebra/CSetoidFun/bpfwdef.con" as lemma.
 330
 331 (*#* Similar for automorphisms. *)
 332
 333 inline procedural "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind".
 334
 335 (* COERCION
 336 cic:/matita/CoRN-Procedural/algebra/CSetoidFun/pfpfun.con
 337 *)
 338
 339 (* NOTATION
 340 Notation Dom := (pfdom _).
 341 *)
 342
 343 (* NOTATION
 344 Notation Part := (pfpfun _).
 345 *)
 346
 347 (* UNEXPORTED
 348 Implicit Arguments pfpfun [S].
 349 *)
 350
 351 (*#*
 352 The next lemma states that every partial function is well defined.
 353 *)
 354
 355 inline procedural "cic:/CoRN/algebra/CSetoidFun/pfwdef.con" as lemma.
 356
 357 (*#*
 358 A few characteristics of this definition should be explained:
 359  - The domain of the partial function is characterized by a predicate
 360 that is required to be well defined but not strongly extensional.  The
 361 motivation for this choice comes from two facts: first, one very
 362 important subset of real numbers is the compact interval
 363 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
 364 [<=] b], which is not strongly extensional; on the other hand, if we
 365 can apply a function to an element [s] of a setoid [S] it seems
 366 reasonable (and at some point we do have to do it) to apply that same
 367 function to any element [s'] which is equal to [s] from the point of
 368 view of the setoid equality.
 369  - The last two conditions state that [pfpfun] is really a subsetoid
 370 function.  The reason why we do not write it that way is the
 371 following: when applying a partial function [f] to an element [s] of
 372 [S] we also need a proof object [H]; with this definition the object
 373 we get is [f(s,H)], where the proof is kept separate from the object.
 374 Using subsetoid notation, we would get $f(\langle
 375 s,H\rangle)$#f(&lang;s,H&rang;)#; from this we need to apply two
 376 projections to get either the original object or the proof, and we
 377 need to apply an extra constructor to get $f(\langle
 378 s,H\rangle)$#f(&lang;s,H&rang;)# from [s] and [H].  This amounts
 379 to spending more resources when actually working with these objects.
 380  - This record has type [Type], which is very unfortunate, because it
 381 means in particular that we cannot use the well behaved set
 382 existential quantification over partial functions; however, later on
 383 we will manage to avoid this problem in a way that also justifies that
 384 we don't really need to use that kind of quantification.  Another
 385 approach to this definition that completely avoid this complication
 386 would be to make [PartFunct] a dependent type, receiving the predicate
 387 as an argument.  This does work in that it allows us to give
 388 [PartFunct] type [Set] and do some useful stuff with it; however, we
 389 are not able to define something as simple as an operator that gets a
 390 function and returns its domain (because of the restrictions in the
 391 type elimination rules).  This sounds very unnatural, and soon gets us
 392 into strange problems that yield very unlikely definitions, which is
 393 why we chose to altogether do away with this approach.
 394
 395 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
 396 %\end{convention}%
 397
 398 We now present some methods for defining partial functions.
 399 *)
 400
 401 (* UNEXPORTED
 402 Hint Resolve CI: core.
 403 *)
 404
 405 (* UNEXPORTED
 406 Section CSetoid_Ops
 407 *)
 408
 409 (* UNEXPORTED
 410 cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/S.var
 411 *)
 412
 413 (*#*
 414 To begin with, we want to be able to ``see'' each total function as a partial function.
 415 *)
 416
 417 inline procedural "cic:/CoRN/algebra/CSetoidFun/total_eq_part.con" as definition.
 418
 419 (* UNEXPORTED
 420 Section Part_Function_Const
 421 *)
 422
 423 (*#*
 424 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
 425
 426 %\begin{convention}% Let [c:S].
 427 %\end{convention}%
 428 *)
 429
 430 (* UNEXPORTED
 431 cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Const/c.var
 432 *)
 433
 434 inline procedural "cic:/CoRN/algebra/CSetoidFun/Fconst.con" as definition.
 435
 436 (* UNEXPORTED
 437 End Part_Function_Const
 438 *)
 439
 440 (* UNEXPORTED
 441 Section Part_Function_Id
 442 *)
 443
 444 inline procedural "cic:/CoRN/algebra/CSetoidFun/Fid.con" as definition.
 445
 446 (* UNEXPORTED
 447 End Part_Function_Id
 448 *)
 449
 450 (*#*
 451 (These happen to be always total functions, but that is more or less obvious, as we have no information on the setoid; however, we will be able to define partial functions just applying other operators to these ones.)
 452
 453 If we have two setoid functions [F] and [G] we can always compose them.  The domain of our new function will be the set of points [s] in the domain of [F] for which [F(s)] is in the domain of [G]#. #%\footnote{%Notice that the use of extension here is essential.%}.%  The inversion in the order of the variables is done to maintain uniformity with the usual mathematical notation.
 454
 455 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
 456 %\end{convention}%
 457 *)
 458
 459 (* UNEXPORTED
 460 Section Part_Function_Composition
 461 *)
 462
 463 (* UNEXPORTED
 464 cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/G.var
 465 *)
 466
 467 (* UNEXPORTED
 468 cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/F.var
 469 *)
 470
 471 (* begin hide *)
 472
 473 inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/P.con" "CSetoid_Ops__Part_Function_Composition__" as definition.
 474
 475 inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/Q.con" "CSetoid_Ops__Part_Function_Composition__" as definition.
 476
 477 (* end hide *)
 478
 479 inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/R.con" "CSetoid_Ops__Part_Function_Composition__" as definition.
 480
 481 inline procedural "cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con" as lemma.
 482
 483 inline procedural "cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con" as lemma.
 484
 485 inline procedural "cic:/CoRN/algebra/CSetoidFun/Fcomp.con" as definition.
 486
 487 (* UNEXPORTED
 488 End Part_Function_Composition
 489 *)
 490
 491 (* UNEXPORTED
 492 End CSetoid_Ops
 493 *)
 494
 495 (*#*
 496 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
 497 %\end{convention}%
 498 *)
 499
 500 (* UNEXPORTED
 501 Section BinPart_Function_Composition
 502 *)
 503
 504 (* UNEXPORTED
 505 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S1.var
 506 *)
 507
 508 (* UNEXPORTED
 509 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S2.var
 510 *)
 511
 512 (* UNEXPORTED
 513 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S3.var
 514 *)
 515
 516 (* UNEXPORTED
 517 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/G.var
 518 *)
 519
 520 (* UNEXPORTED
 521 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/F.var
 522 *)
 523
 524 (* begin hide *)
 525
 526 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/P.con" "BinPart_Function_Composition__" as definition.
 527
 528 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/Q.con" "BinPart_Function_Composition__" as definition.
 529
 530 (* end hide *)
 531
 532 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/R.con" "BinPart_Function_Composition__" as definition.
 533
 534 inline procedural "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con" as lemma.
 535
 536 inline procedural "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con" as lemma.
 537
 538 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinFcomp.con" as definition.
 539
 540 (* UNEXPORTED
 541 End BinPart_Function_Composition
 542 *)
 543
 544 (* Different tokens for compatibility with coqdoc *)
 545
 546 (* UNEXPORTED
 547 Implicit Arguments Fconst [S].
 548 *)
 549
 550 (* NOTATION
 551 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
 552 *)
 553
 554 (* NOTATION
 555 Notation FId := (Fid _).
 556 *)
 557
 558 (* UNEXPORTED
 559 Implicit Arguments Fcomp [S].
 560 *)
 561
 562 (* NOTATION
 563 Infix "[o]" := Fcomp (at level 65, no associativity).
 564 *)
 565
 566 (* UNEXPORTED
 567 Hint Resolve pfwdef bpfwdef: algebra.
 568 *)
 569
 570 (* UNEXPORTED
 571 Section bijections
 572 *)
 573
 574 (*#* **Bijections *)
 575
 576 inline procedural "cic:/CoRN/algebra/CSetoidFun/injective.con" as definition.
 577
 578 inline procedural "cic:/CoRN/algebra/CSetoidFun/injective_weak.con" as definition.
 579
 580 inline procedural "cic:/CoRN/algebra/CSetoidFun/surjective.con" as definition.
 581
 582 (* UNEXPORTED
 583 Implicit Arguments injective [A B].
 584 *)
 585
 586 (* UNEXPORTED
 587 Implicit Arguments injective_weak [A B].
 588 *)
 589
 590 (* UNEXPORTED
 591 Implicit Arguments surjective [A B].
 592 *)
 593
 594 inline procedural "cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con" as lemma.
 595
 596 inline procedural "cic:/CoRN/algebra/CSetoidFun/bijective.con" as definition.
 597
 598 (* UNEXPORTED
 599 Implicit Arguments bijective [A B].
 600 *)
 601
 602 inline procedural "cic:/CoRN/algebra/CSetoidFun/id_is_bij.con" as lemma.
 603
 604 inline procedural "cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con" as lemma.
 605
 606 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv.con" as lemma.
 607
 608 (* UNEXPORTED
 609 Implicit Arguments inv [A B].
 610 *)
 611
 612 inline procedural "cic:/CoRN/algebra/CSetoidFun/invfun.con" as definition.
 613
 614 (* UNEXPORTED
 615 Implicit Arguments invfun [A B].
 616 *)
 617
 618 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv1.con" as lemma.
 619
 620 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv2.con" as lemma.
 621
 622 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv_strext.con" as lemma.
 623
 624 inline procedural "cic:/CoRN/algebra/CSetoidFun/Inv.con" as definition.
 625
 626 (* UNEXPORTED
 627 Implicit Arguments Inv [A B].
 628 *)
 629
 630 inline procedural "cic:/CoRN/algebra/CSetoidFun/Inv_bij.con" as definition.
 631
 632 (* UNEXPORTED
 633 End bijections
 634 *)
 635
 636 (* UNEXPORTED
 637 Implicit Arguments bijective [A B].
 638 *)
 639
 640 (* UNEXPORTED
 641 Implicit Arguments injective [A B].
 642 *)
 643
 644 (* UNEXPORTED
 645 Implicit Arguments injective_weak [A B].
 646 *)
 647
 648 (* UNEXPORTED
 649 Implicit Arguments surjective [A B].
 650 *)
 651
 652 (* UNEXPORTED
 653 Implicit Arguments inv [A B].
 654 *)
 655
 656 (* UNEXPORTED
 657 Implicit Arguments invfun [A B].
 658 *)
 659
 660 (* UNEXPORTED
 661 Implicit Arguments Inv [A B].
 662 *)
 663
 664 (* UNEXPORTED
 665 Implicit Arguments conj_wd [S P Q].
 666 *)
 667
 668 (* NOTATION
 669 Notation Prj1 := (prj1 _ _ _ _).
 670 *)
 671
 672 (* NOTATION
 673 Notation Prj2 := (prj2 _ _ _ _).
 674 *)
 675