proposition: Lemma zero_gseq_r: forall r s t (R : paco2 gseq_step r s t), paco2 gseq_step r s (scons 0 t).
proof: Proof. intros. punfold R. pfold. destruct R; eauto. econstructor; eauto. pfold. eauto. Qed.
imports: ZArith List String Paco.paco Program Classical