proposition: Lemma is_finite_for_iff ls f : is_finite_for ls f <-> @is_finite_forA A eq bot B (B -> A) eq (fun f => f) ls f.
proof: Proof. unfold is_finite_for, is_finite_forA, is_finite_forA'. setoid_rewrite InA_alt. split; intros H x H'; apply H; intro H''; apply H'. { eexists; split; [ reflexivity | assumption ]. } { destruct H'' as [? [? ?]]; subst; assumption. } Qed.
imports: Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf Coq.Lists.SetoidList Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat