proposition: Lemma gseq_implies_seq: forall s t (R: gseq s t), seq s t.
proof: Proof. pcofix CIH; intros. punfold R. destruct R. - punfold IZ1. punfold IZ2. dependent destruction IZ1. dependent destruction IZ2. pclearbot. pfold. econstructor. right. eauto. - induction ZS1; subst. + induction ZS2; subst. * pfold. dependent destruction R; pclearbot; eauto. * pfold. punfold IHZS2. + pfold. punfold IHZS1. Qed.
imports: ZArith List String Paco.paco Program Classical