fact: Axiom thm_ALLPAIRS_SYM : forall {_36263 _36264 : Type'}, forall P : _36264 -> _36263 -> Prop, forall l : list _36264, forall m : list _36263, (@ALLPAIRS _36263 _36264 P l m) = (@ALLPAIRS _36264 _36263 (fun x : _36263 => fun y : _36264 => P y x) m l).
imports: coq theory_hol types terms axioms