<div dir="ltr">Hi There!<div><br></div><div>Unfortunately I have ran into a problem for translating PART3 in SortingTheory from HOL4 to CakeML. </div><div><br></div><div>I was wondering if this problem could be resolved ASAP? I really need this translation to go through. </div><div><br></div><div>many thanks for your guidance,</div><div>Milad</div></div>