proposition: Lemma exists_element_list: forall {A B: Type} {A': Inhabitant A} {B': Inhabitant B} (P: A -> B -> Prop) (la: list A), (forall a, In a la -> exists b, P a b) -> (exists lb, Zlength lb = Zlength la /\ forall i, 0 <= i < Zlength la -> P (Znth i la) (Znth i lb)).
proof: Proof. induction la; intros. exists nil. split. auto. intros. rewrite Zlength_nil in H0; lia. assert (forall a : A, In a la -> exists b : B, P a b). intros. apply H. right; auto. apply IHla in H0. destruct H0 as [lb ?]. assert (exists b : B, P a b). apply H. left; auto. destruct H1 as [b ?]. exists (b::lb). split. do 2 rewrite Zlength_cons; lia. intros. rewrite Zlength_cons in H2. destruct (Z.lt_trichotomy 0 i). do 2 rewrite Znth_pos_cons by lia. apply H0. lia. destruct H3. subst i. do 2 rewrite Znth_0_cons. auto. lia. 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