fact: CoFixpoint park_ppl : forall s1 s2:Stream A, R s1 s2 -> EqSt s1 s2 := fun s1 s2 (p : R s1 s2) => eqst s1 s2 (bisim1 p) (park_ppl (bisim2 p)).
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool