fact: Axiom thm_MEM_ASSOC : forall {_36008 _36024 : Type'}, forall l : list (prod _36024 _36008), forall x : _36024, (@List.In (prod _36024 _36008) (@pair _36024 _36008 x (@ASSOC _36008 _36024 x l)) l) = (@List.In _36024 x (@List.map (prod _36024 _36008) _36024 (@fst _36024 _36008) l)).
imports: coq theory_hol types terms axioms