fact: Axiom thm_AND_ALL2 : forall {_36232 _36233 : Type'}, forall P : _36233 -> _36232 -> Prop, forall Q : _36233 -> _36232 -> Prop, forall l : list _36233, forall m : list _36232, ((@ALL2 _36233 _36232 P l m) /\ (@ALL2 _36233 _36232 Q l m)) = (@ALL2 _36233 _36232 (fun x : _36233 => fun y : _36232 => (P x y) /\ (Q x y)) l m).
imports: coq theory_hol types terms axioms