fact: Fixpoint first_st_at A (P:A->Prop) (s:stream A) (n:nat) := let '(x:::s') := s in match n with | O => P x | S n' => ~ P x /\ first_st_at P s' n' end.
imports: TLC(LibTactics LibLogic LibInt LibList LibRelation LibWf)