proposition: Lemma list_eq_Znth: forall {A:Type} {d: Inhabitant A} (l l': list A), Zlength l = Zlength l' -> (forall i, 0 <= i < Zlength l -> Znth i l = Znth i l') -> l = l'.
proof: Proof. induction l; intros. symmetry; apply Zlength_nil_inv. rewrite Zlength_nil in H; auto. destruct l'. rewrite Zlength_cons, Zlength_nil in H. pose proof (Zlength_nonneg (A:=A) l). assert (Zlength l < Z.succ (Zlength l)) by lia. lia. replace a with (Znth 0 (a::l)). 2: rewrite Znth_0_cons; auto. replace a0 with (Znth 0 (a0::l)). 2: rewrite Znth_0_cons; auto. rewrite (H0 0). 2: rewrite Zlength_cons; pose proof (Zlength_nonneg (A:=A) l); lia. rewrite (IHl l'); auto. apply Z.succ_inj. do 2 rewrite Zlength_cons in H. auto. intros. replace (Znth i l) with (Znth (i+1) (a::l)). replace (Znth i l') with (Znth (i+1) (a0::l')). apply H0. rewrite Zlength_cons. lia. replace (Znth i l') with (Znth (i+1 - 1) l'). apply Znth_pos_cons. lia. rewrite Z.add_simpl_r; auto. replace (Znth i l) with (Znth (i+1 - 1) l). apply Znth_pos_cons. lia. rewrite Z.add_simpl_r; auto. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver