FORALL_UNWIND_CONV : term -> thm
- SYNOPSIS
-
Eliminates universally quantified variables that are equated to something.
- DESCRIPTION
-
The conversion FORALL_UNWIND_CONV, applied to a formula with one or more
universal quantifiers around an implication, eliminates any quantifiers where
the antecedent of the implication contains a conjunct equating its variable to
some other term (with that variable not free in it).
- FAILURE CONDITIONS
-
FORALL_UNWIND_CONV tm fails if tm is not reducible according to that
description.
- EXAMPLE
-
# FORALL_UNWIND_CONV
`!a b c d. a + 1 = b /\ b + 1 = c + 1 /\ d = e ==> a + b + c + d + e = 2`;;
val it : thm =
|- (!a b c d.
a + 1 = b /\ b + 1 = c + 1 /\ d = e ==> a + b + c + d + e = 2) <=>
(!a c. (a + 1) + 1 = c + 1 ==> a + (a + 1) + c + e + e = 2)
# FORALL_UNWIND_CONV `!a b c. a = b /\ b = c ==> a + b = b + c`;;
val it : thm =
|- (!a b c. a = b /\ b = c ==> a + b = b + c) <=> (!c. c + c = c + c)
- SEE ALSO
-
UNWIND_CONV.