fact: Axiom thm_ALL_MP : forall {_35494 : Type'}, forall P : _35494 -> Prop, forall Q : _35494 -> Prop, forall l : list _35494, ((@List.Forall _35494 (fun x : _35494 => (P x) -> Q x) l) /\ (@List.Forall _35494 P l)) -> @List.Forall _35494 Q l.
imports: coq theory_hol types terms axioms