Changeset 2111 for src/common
- Timestamp:
- Jun 26, 2012, 5:30:41 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Identifiers.ma
r1949 r2111 80 80 @(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ] 81 81 qed. 82 83 lemma 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 ] 103 qed. 104 105 axiom neq_identifier_neq: 106 ∀tag: String. 107 ∀l, r: identifier tag. 108 eq_identifier tag l r = false → (l = r → False). 82 109 83 110 include "basics/deqsets.ma".
Note: See TracChangeset
for help on using the changeset viewer.