FORALL_UNWIND_CONV : term -> thm
# 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)