Changeset 2111 for src/common


Ignore:
Timestamp:
Jun 26, 2012, 5:30:41 PM (7 years ago)
Author:
sacerdot
Message:

Cleanup: lemmas/theorems/axioms moved to the right places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1949 r2111  
    8080@(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
    8181qed.
     82
     83lemma eq_identifier_eq:
     84  ∀tag: String.
     85  ∀l.
     86  ∀r.
     87    eq_identifier tag l r = true → l = r.
     88  #tag #l #r cases l cases r
     89  #pos_l #pos_r
     90  cases pos_l cases pos_r
     91  [1:
     92    #_ %
     93  |2,3,4,7:
     94    #p1_l normalize in ⊢ (% → ?);
     95    #absurd destruct(absurd)
     96  |5,9:
     97    #p1_l #p1_r normalize in ⊢ (% → ?);
     98    #relevant lapply (eqb_true_to_eq … relevant) #EQ >EQ %
     99  |*:
     100    #p_l #p_r normalize in ⊢ (% → ?);
     101    #absurd destruct(absurd)
     102  ]
     103qed.
     104
     105axiom neq_identifier_neq:
     106  ∀tag: String.
     107  ∀l, r: identifier tag.
     108    eq_identifier tag l r = false → (l = r → False).
    82109
    83110include "basics/deqsets.ma".
Note: See TracChangeset for help on using the changeset viewer.