proposition: Lemma equiv_clogs_impl: forall n L1 L2, Equiv L1 L2 -> Equiv (Clogs L1 n) (Clogs L2 n).
proof: Proof. intros. unfold Clogs; split; unfold In; intros; subst. - assert (H0 := H0 x y z eq_refl H2 H3). destruct H0 as (i, Hx). exists i. intros N. contradict Hx. apply H. assumption. - assert (H0 := H0 x y z eq_refl H2 H3). destruct H0 as (i, Hx). exists i. intros N. contradict Hx. apply 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