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