fact: Axiom thm_FORALL_UNPAIR_THM : forall {_5486 _5488 : Type'}, forall P : _5486 -> _5488 -> Prop, (forall x : _5486, forall y : _5488, P x y) = (forall z : prod _5486 _5488, P (@fst _5486 _5488 z) (@snd _5486 _5488 z)).
imports: coq theory_hol types terms axioms