proposition: Lemma upd_Znth_same_Znth: forall {A} `{Ia : Inhabitant A} (l: list A) i, 0 <= i < Zlength l -> upd_Znth i l (Znth i l) = l.
proof: Proof. intros. rewrite upd_Znth_unfold by trivial. rewrite <- sublist_len_1 by trivial. repeat rewrite <- sublist_split. apply sublist_same; trivial. all: lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model