proposition: Lemma in_map_iffT_nat {A} (f : A -> nat) (ls : list A) (y : nat) : iffT (In y (map f ls)) { x : A | f x = y /\ In x ls }.
proof: Proof. apply in_map_iffT, Nat.eq_dec. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts