proposition: Lemma co_red_2: forall A B, A <=m compl B -> compl A <=m B.
proof: Proof. intros. assert (R: Equiv A (compl (compl A))) 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