Let's say I have a goal,
a /\ b /\ c ==> d
and 2 theorems
a /\ b ==> e
e ==> f
All I need to do to solve the goal is rewrite using a theorem that states
`f`, however I need to first prove e, which is only probable because the
goal assumes `a`.
The basis of my question, is whether or not I can use an assumption of the
goal outside of a tactical. My proof would be a lot more readable if I
could use `a` and `b` to "prove" `e` outside of a tactical application like
ASSUM_LIST and similar tactics require.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
