Hi Dylan, What I would try in HOL Light:
# g `a ==> b /\ c ==> d /\ e ==> k`;; Warning: Free variables in goal: a, b, c, d, e, k val it : goalstack = 1 subgoal (1 total) `a ==> b /\ c ==> d /\ e ==> k` # e (REPEAT DISCH_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`a`] 1 [`b /\ c`] 2 [`d /\ e`] `k` # e (POP_ASSUM_LIST (MAP_EVERY (MAP_EVERY ASSUME_TAC) o rev o map CONJUNCTS));; val it : goalstack = 1 subgoal (1 total) 0 [`a`] 1 [`b`] 2 [`c`] 3 [`d`] 4 [`e`] `k` # Freek ------------------------------------------------------------------------------ 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
