Changeset 882 for src/utilities/extralib.ma
 Timestamp:
 Jun 3, 2011, 5:35:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r711 r882 387 387 definition div ≝ λm,n. fst ?? (divide m n). 388 388 definition mod ≝ λm,n. snd ?? (divide m n). 389 390 definition pairdisc ≝391 λA,B.λx,y:Prod A B.392 match x with393 [(pair t0 t1) ⇒394 match y with395 [(pair u0 u1) ⇒396 ∀P: Type[1].397 (∀e0: (eq A (R0 ? t0) u0).398 ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].399 400 lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.401 #A #B #x #y #e >e cases y;402 #a #b normalize;#P #PH @PH %403 qed.404 389 405 390 lemma pred_minus: ∀n,m. pred n  m = pred (nm).
Note: See TracChangeset
for help on using the changeset viewer.