proposition: Lemma upd_Znth_repeat_app {X: Type} {IX: Inhabitant X}: forall i (vh v0 v1 v2: X) l, 1 <= i -> upd_Znth i (vh :: repeat v0 (Z.to_nat (i - 1)) ++ v1 :: l) v2 = vh :: repeat v0 (Z.to_nat (i - 1)) ++ v2 :: l.
proof: Proof. intros. rewrite app_comm_cons, upd_Znth_app2. - rewrite app_comm_cons. f_equal. rewrite Zlength_cons, Zlength_repeat by lia. replace (i - Z.succ (i - 1)) with 0 by lia. rewrite upd_Znth0. f_equal. - rewrite Zlength_cons, !Zlength_repeat by lia. replace (Z.succ (i - 1)) with i by lia. pose proof (Zlength_nonneg (v1 :: l)). lia. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)