fact: Axiom thm_ALL_APPEND : forall {_36045 : Type'}, forall P : _36045 -> Prop, forall l1 : list _36045, forall l2 : list _36045, (@List.Forall _36045 P (@List.app _36045 l1 l2)) = ((@List.Forall _36045 P l1) /\ (@List.Forall _36045 P l2)).
imports: coq theory_hol types terms axioms