proposition: Lemma co_a_tm_red_co_self_tm: compl SELF_tm <=m compl A_tm.
proof: Proof. intros. exists (fun i => <[ decode_mach i, i ]>). unfold Reduction. intros. unfold A_tm, SELF_tm, compl; split; intros. - intros N1. contradict H. run_simpl. assumption. - intros N1. contradict H. run_simpl. assumption. Qed.
imports: Coq.Setoids.Setoid Turing.Turing Turing.LangDec Turing.LangRed