proposition: Lemma co_red_co_2: forall A B, compl A <=m compl B -> A <=m B.
proof: Proof. intros. unfold Reducible in *. destruct H as (f, Hr). unfold Reduction in *. exists f. intros. unfold compl. split; intros. + apply co_co_rw. intros N. apply Hr in N. contradiction. + apply co_co_rw. intros N. apply Hr in N. contradiction. Qed.
imports: Coq.Setoids.Setoid Turing.Turing