Ignore:
Timestamp:
Jun 3, 2011, 5:35:32 PM (9 years ago)
Author:
campbell
Message:

Fix up fragile proofs for current version of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r711 r882  
    387387definition div ≝ λm,n. fst ?? (divide m n).
    388388definition mod ≝ λm,n. snd ?? (divide m n).
    389 
    390 definition pairdisc ≝
    391 λA,B.λx,y:Prod A B.
    392 match x with
    393 [(pair t0 t1) ⇒
    394 match y with
    395 [(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.
    404389
    405390lemma pred_minus: ∀n,m. pred n - m = pred (n-m).
Note: See TracChangeset for help on using the changeset viewer.