proposition: Lemma forall_in_eq_key_elt_snd {A} ls (P : _ -> Prop) : (forall x : key * A, List.In x ls -> P (snd x)) <-> (forall x : key * A, InA (@eq_key_elt A) x ls -> P (snd x)).
proof: Proof. split; intros H x H'. { rewrite InA_alt in H'. destruct H' as [y [[H'0 ?] H'1]]. specialize (H y); destruct y; simpl in *; subst. eauto. } { apply H. apply InA_In; [ exact _ | ]. assumption. } Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances