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