Changeset 993 for src/ASM/Util.ma


Ignore:
Timestamp:
Jun 17, 2011, 6:28:49 PM (8 years ago)
Author:
sacerdot
Message:

More Russell everywhere; getting closer to the goal.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r990 r993  
    211211for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
    212212
     213axiom 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
     221axiom 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
     230lemma pair_destruct_1:
     231 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
     232 #A #B #a #b *; /2/
     233qed.
     234
     235lemma pair_destruct_2:
     236 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
     237 #A #B #a #b *; /2/
     238qed.
     239
     240
    213241notation "⊥" with precedence 90
    214242  for @{ match ? in False with [ ] }.
Note: See TracChangeset for help on using the changeset viewer.