fact: CoInductive EqSt (A: Set) : Stream A -> Stream A -> Prop := eqst : forall s1 s2: Stream A, head s1 = head s2 -> EqSt (tail s1) (tail s2) -> EqSt s1 s2.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool