Changeset 1598 for src/ASM/FoldStuff.ma


Ignore:
Timestamp:
Dec 12, 2011, 5:53:36 PM (8 years ago)
Author:
mulligan
Message:

changes over the last couple of days

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/FoldStuff.ma

    r1062 r1598  
    4848 ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …).
    4949
    50 lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
     50lemma pair_destruct: ∀A,B,a1,a2,b1,b2. mk_Prod A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
    5151 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
    5252qed.
Note: See TracChangeset for help on using the changeset viewer.