proposition: Lemma zeros_star_nonzero_uniq: forall s1 s2 t (ZS1: zeros_star (fun s => s = s1) t) (ZS2: zeros_star (fun s => s = s2) t) (NZ1: nonzero s1) (NZ2: nonzero s2), s1 = s2.
proof: Proof. intros s1 s2 t ZS1. revert s2. induction ZS1; subst; intros. - induction ZS2; subst; eauto. inversion NZ1. intuition. - dependent destruction ZS2; eauto. inversion NZ2. intuition. Qed.
imports: ZArith List String Paco.paco Program Classical