Fill in an admit

theories/DisjointSetUnionCode2.v

@@ -513,7 +513,7 @@ Proof.
            end) vardef_0__unite_u
         (Z.of_nat (ancestor dsu (length dsu) (Z.to_nat a))) = fun x => match x with | vardef_0__unite_u => Z.of_nat (ancestor dsu (length dsu) (Z.to_nat a)) | vardef_0__unite_v => b | vardef_0__unite_z => 0%Z end). { apply functional_extensionality_dep. intro hh. destruct hh; easy. } rewrite le. clear le.
   unfold numberLocalGet at 1. rewrite pushNumberGet2 !leftIdentity eliminateLift.
-  rewrite -!bindAssoc runAncestor; try (assumption || lia). { rewrite pathCompressPreservesLength; (assumption || lia). } { rewrite pathCompressPreservesLength; try (assumption || lia). rewrite pathCompressPreservesLeafCount; try (assumption || lia). } { admit. } { rewrite pathCompressPreservesLength; try (assumption || lia). apply pathCompressPreservesWithoutCycles; try (assumption || lia). } unfold retrieve at 1. rewrite !pushDispatch2 (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Retrieve. case_decide as ppp; [| simpl in ppp; lia]. rewrite (ltac:(intros; easy) : forall a c, nth_lt [a] (Z.to_nat 0%Z) c = a). clear ppp. unfold numberLocalSet at 1. rewrite pushNumberSet2.
+  rewrite -!bindAssoc runAncestor; try (assumption || lia). { rewrite pathCompressPreservesLength; (assumption || lia). } { rewrite pathCompressPreservesLength; try (assumption || lia). rewrite pathCompressPreservesLeafCount; try (assumption || lia). } { apply pathCompressPreservesNoIllegalIndices; try (assumption || lia). apply ancestorLtLength; try assumption. lia. } { rewrite pathCompressPreservesLength; try (assumption || lia). apply pathCompressPreservesWithoutCycles; try (assumption || lia). } unfold retrieve at 1. rewrite !pushDispatch2 (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Retrieve. case_decide as ppp; [| simpl in ppp; lia]. rewrite (ltac:(intros; easy) : forall a c, nth_lt [a] (Z.to_nat 0%Z) c = a). clear ppp. unfold numberLocalSet at 1. rewrite pushNumberSet2.
   assert (uwl : update
         (λ _0 : varsfuncdef_0__unite,
            match _0 with