dest_forall : term -> term * term
- SYNOPSIS
-
Breaks apart a universally quantified term into quantified variable and body.
- DESCRIPTION
-
dest_forall is a term destructor for universal quantification:
dest_forall `!var. t` returns (`var`,`t`).
- FAILURE CONDITIONS
-
Fails with dest_forall if term is not a universal quantification.
- SEE ALSO
-
is_forall, mk_forall, strip_forall.