proposition: Lemma in_clogs: forall w p L, (forall x y z, w = x ++ y ++ z -> y <> [] -> length (x ++ y) <= p -> exists i, ~ In (x ++ (pow y i) ++ z) L) -> In w (Clogs L p).
proof: Proof. intros. unfold Clogs. intros; auto. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util