instantiate : instantiation -> term -> term
# let t = `(!x. P x) <=> ~(?x. P x)`;; Warning: inventing type variables val t : term = `(!x. P x) <=> ~(?x. P x)` # let i = term_match [] (lhs t) `!p. prime(p) ==> p = 2 \/ ODD(p)`;; val i : instantiation = ([(1, `P`)], [(`\p. prime p ==> p = 2 \/ ODD p`, `P`)], [(`:num`, `:?61195`)])
# instantiate i t;; val it : term = `(!x. prime x ==> x = 2 \/ ODD x) <=> ~(?x. prime x ==> x = 2 \/ ODD x)`