Hello everyone!<br><br>In stdlib-0.6 we have:<br>data Any {a p} {A : Set a} (P : A → Set p) : List A → Set (a ⊔ p) where<br>  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)<br>  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)<br>
<br>When I didn&#39;t know about it, I tried to do it in the following way:<br>data Any {A : Set} (P : A → Set) : List A → Set where<br>  exact : ∀ {x} l r → P x → Any P (l ++ x ∷ r)<br><br>For the reasoning I needed a function:<br>
AnyP[h∷t]⇒Ph⊎AnyPt : {A : Set} {P : A → Set} {h : A} {t : List A} → Any P (h ∷ t) → P h ⊎ Any P t<br>AnyP[h∷t]⇒Ph⊎AnyPt .{h = x} .{t = r} (exact {x = x} [] r p) = _<br>AnyP[h∷t]⇒Ph⊎AnyPt .{h = l} .{t = ls ++ x ∷ r} (exact {x = x} (l ∷ ls) r p) = _<br>
<br>But I got stuck in implementation.<br>Could you please help me with it?<br>*I don&#39;t need such &quot;Any&quot; type, but I am interested whether it is possible to do it. And if it is not possible, then why?<br>**I think here some information might be missed like in square function: having x^2 we don&#39;t know whether x is positive or negative.<br>
<br>Thank you,<br>Dmytro<br>