move v_to_exh_extend_disjoint to exhLangProofScript.sml