proposition: Lemma alist_ind : forall (A : Type) (P : list (X.t * A) -> Type), (P nil) -> (forall x a xs, P xs -> P (x ~ a ++ xs)) -> (forall xs, P xs).
proof: Proof. induction xs as [ | [x a] xs ]. auto. change (P (x ~ a ++ xs)). auto. Defined.
imports: Coq.FSets.FSets Coq.Lists.List Coq.Logic.Decidable Coq.Strings.String String Metalib.CoqFSetDecide Metalib.CoqListFacts Metalib.LibTactics Metalib.CoqFSetInterface Coq.Classes.Equivalence Coq.Classes.EquivDec Metalib.CoqEqDec