@@ -75,3 +75,8 @@ all d (x::xs) with (d x)
75 case all d xs of
75 case all d xs of
76 Yes prf' => Yes (prf :: prf')
76 Yes prf' => Yes (prf :: prf')
77 No prf' => No (notAllThere prf')
77 No prf' => No (notAllThere prf')
79+||| Given a proof of membership for some element, extract the property proof for it
80+indexAll : Elem x xs -> All p xs -> p x
81+indexAll Here (p::_ ) = p
82+indexAll (There e) ( _::ps) = indexAll e ps