Hint Unfoldeqkeqke : core. Hint Extern 2 (eqke ?a ?b) => split : core. Hint Resolveeqk_transeqke_transeqk_refleqke_refl : core. Hint Immediateeqk_symeqke_sym : core. Hint ResolveInA_eqke_eqk : core. Hint UnfoldMapsToIn : core. Hint ResolveIn_inv_2In_inv_3 : core.