proposition: Lemma seq_infzeros_imply: forall s t (R: seq s t) (IZ: infzeros s), infzeros t.
proof: Proof. pcofix CIH. intros. punfold R. revert IZ. induction R; intros. - eapply paco1_mon. eauto. intros. inversion PR. - pfold. punfold IZ. dependent destruction IZ. pclearbot. eauto. - punfold IZ. dependent destruction IZ. pclearbot. eauto. - pfold. eauto. Qed.
imports: ZArith List String Paco.paco Program Classical