proposition: Lemma co_red_1: forall A B, compl A <=m B -> A <=m compl B.
proof: Proof. intros. assert (R: Equiv B (compl (compl B))) by (rewrite co_co_rw; reflexivity). rewrite R in H. rewrite co_red_co_rw in H. assumption. Qed.
imports: Coq.Setoids.Setoid Turing.Turing