As a more concise question: can you use assumptions of the hypothesis to
eliminate the assumptions of a theorem?
On Mon, Aug 20, 2018, 4:51 PM Dylan Melville <dylanmelvi...@gmail.com>
wrote:
> 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
