fact: Axiom thm_ALLPAIRS_MAP : forall {_36342 _36343 _36344 _36345 : Type'} (f : _36344 -> _36343) (g : _36345 -> _36342), forall P : _36343 -> _36342 -> Prop, forall l : list _36344, forall m : list _36345, (@ALLPAIRS _36342 _36343 P (@List.map _36344 _36343 f l) (@List.map _36345 _36342 g m)) = (@ALLPAIRS _36345 _36344 (fun x : _36344 => fun y : _36345 => P (f x) (g y)) l m).
imports: coq theory_hol types terms axioms