ConseqConv.FORALL_EQ___CONSEQ

FORALL_EQ___CONSEQ_CONV : conseq_conv

STRUCTURE: ConseqConv
SYNOPSIS: Given a term of the form (!x. P x) = (!x. Q x) this consequence conversion returns the theorem |- (!x. (P x = Q x)) ==> ((!x. P x) = (!x. Q x)).
SEEALSO: conseq_conv

HOL Kananaskis-13