proposition: Lemma in_map_iffT' {A B} (f : A -> B) (ls : list A) (y : B) (eq_dec : forall y', {y = y'} + {y <> y'}) : iffT (In y (map f ls)) { x : A | f x = y /\ In x ls }.
proof: Proof. split; [ | intros [x H]; apply in_map_iff; exists x; assumption ]. induction ls as [|l ls IHls]. { simpl; intros []. } { simpl. intro H. destruct (eq_dec (f l)) as [e|e]. { exists l; split. { clear -e; abstract (subst; reflexivity). } { left. reflexivity. } } { destruct IHls as [x H']. { clear -H e. abstract (destruct H; congruence). } { eexists. split; [ apply H' | right; apply H' ]. } } } 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