proposition: Lemma Znth_repeat_app {X: Type} {IX: Inhabitant X}: forall i (vh v0 vn: X) l, 1 <= i -> Znth i (vh :: repeat v0 (Z.to_nat (i - 1)) ++ vn :: l) = vn.
proof: Proof. intros. rewrite Znth_pos_cons by lia. rewrite app_Znth2 by (rewrite Zlength_repeat; lia). rewrite Zlength_repeat by lia. replace (i - 1 - (i - 1)) with 0 by lia. rewrite Znth_0_cons. reflexivity. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)