proposition: Lemma seq_zeros_star_imply: forall s t (R: seq s t) (IZ: zeros_star nonzero s), zeros_star nonzero t.
proof: Proof. intros. revert t R. induction IZ; intros. - punfold R. induction R; pclearbot; eauto. + inversion BASE. eauto. + inversion BASE. intuition. - punfold R. remember(scons 0 t). generalize dependent t. induction R; intros; pclearbot; dependent destruction Heqs; eauto. Qed.
imports: ZArith List String Paco.paco Program Classical