Changeset 2292 for src/utilities
 Timestamp:
 Aug 2, 2012, 6:40:15 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/lists.ma
r1949 r2292 76 76 [ * [ //  #h #t #_ * ] 77 77  #ha #ta #IH * [ //  #hb #tb #H * #H1 #H2 % [ @H @H1  @(IH … H2) @H ] ] 78 ] qed. 79 80 lemma All2_left : ∀A,B,P,la,lb. 81 All2 A B P la lb → All A (λa.∃b.P a b) la. 82 #A #B #P #la elim la 83 [ // 84  #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hdb} //  /2/ ] 85 ] qed. 86 87 lemma All2_right : ∀A,B,P,la,lb. 88 All2 A B P la lb → All B (λb.∃a.P a b) lb. 89 #A #B #P #la elim la 90 [ * // #h #t * 91  #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hda} //  /2/ ] 78 92 ] qed. 79 93
Note: See TracChangeset
for help on using the changeset viewer.