proposition: Lemma equiv_clogged: forall L1 L2 p, Equiv L1 L2 -> Clogged L1 p -> Clogged L2 p.
proof: Proof. intros. inversion H0; subst; clear H0. apply clogged_def with (w:=w). - apply H. assumption. - assumption. - apply equiv_clogs_impl with (n:=p) in H. rewrite <- H. assumption. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util