proposition: Lemma InList_ind_helper : forall {A : Type} {P : A -> Prop} {x : A} {xs : list A}, (forall k, List.In k (x :: xs) -> P k) -> (P x /\ (forall k, List.In k xs -> P k)).
proof: Proof. intros; split; intros; eapply H; simpl; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.Structures.OrderedTypeEx