proposition: Lemma co_co_rw: forall L, Equiv (compl (compl L)) L.
proof: Proof. intros. unfold Equiv. split; intros. { destruct (Classical_Prop.classic (L i)). { assumption. } apply H in H0. inversion H0. } unfold compl. intros N. contradiction. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop