proposition: Lemma seq_implies_gseq: forall s t (R: seq s t), gseq s t.
proof: Proof. pcofix CIH. intros. destruct (seq_infzeros_or_finzeros R) as [[]|[]]; eauto. induction H. - induction H0. + pfold. punfold R. dependent destruction R; pclearbot; eauto. * dependent destruction BASE. eauto 10. * dependent destruction BASE. intuition. * dependent destruction BASE0. intuition. + eauto using seq_zero_r, zero_gseq_r. - eauto using seq_zero_l, zero_gseq_l. Qed.
imports: ZArith List String Paco.paco Program Classical