proposition: Lemma seq_zero_r: forall s t (EQ : seq s (scons 0 t)), seq s t.
proof: Proof. intros. punfold EQ. pfold. remember (scons 0 t). generalize dependent t. induction EQ; intros; dependent destruction Heqs0; pclearbot; eauto. punfold R. Qed.
imports: ZArith List String Paco.paco Program Classical