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