#M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
#t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
#q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
% [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
qed.
#M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
#t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
#q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
% [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
qed.