proposition: Lemma in_map_unproject : forall {A B} projection seq, forall item, @List.In A item seq -> @List.In B (projection item) (List.map projection seq).
proof: Proof. intros ? ? ? seq; induction seq; simpl; intros item in_seq. trivial. destruct in_seq; [ left; f_equal | right ]; intuition. Qed.
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