Changeset 993 for src/ASM/Util.ma
 Timestamp:
 Jun 17, 2011, 6:28:49 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r990 r993 211 211 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }. 212 212 213 axiom pair_elim': 214 ∀A,B,C: Type[0]. 215 ∀T: A → B → C. 216 ∀p. 217 ∀P: A×B → C → Prop. 218 (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) → 219 P p (let 〈lft, rgt〉 ≝ p in T lft rgt). 220 221 axiom pair_elim'': 222 ∀A,B,C,C': Type[0]. 223 ∀T: A → B → C. 224 ∀T': A → B → C'. 225 ∀p. 226 ∀P: A×B → C → C' → Prop. 227 (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) → 228 P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt). 229 230 lemma pair_destruct_1: 231 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c. 232 #A #B #a #b *; /2/ 233 qed. 234 235 lemma pair_destruct_2: 236 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c. 237 #A #B #a #b *; /2/ 238 qed. 239 240 213 241 notation "⊥" with precedence 90 214 242 for @{ match ? in False with [ ] }.
Note: See TracChangeset
for help on using the changeset viewer.