Changeset 1598 for src/ASM/FoldStuff.ma
 Timestamp:
 Dec 12, 2011, 5:53:36 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/FoldStuff.ma
r1062 r1598 48 48 ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …). 49 49 50 lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pairA B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.50 lemma pair_destruct: ∀A,B,a1,a2,b1,b2. mk_Prod A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2. 51 51 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/ 52 52 qed.
Note: See TracChangeset
for help on using the changeset viewer.