fact: Definition map (f1 : A -> A) (f2: B -> B) (E : list (asn A B)) : list (asn A B) := List.map (fun x => match x with | VarAsn _ x a => VarAsn B x (f1 a) | AltAsn _ b => AltAsn A (f2 b) end) E.
imports: Coq.FSets.FSets Coq.Lists.List Coq.Logic.Decidable Metalib.CoqFSetDecide Metalib.CoqListFacts Metalib.LibTactics Metalib.MetatheoryAtom Metalib.LibTactics