On 19/12/17 09:27, Mario Castelán Castro wrote: > Maybe this is what you want: > > prove( > “(∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2)”, > disch_then strip_assume_tac >> > rpt BasicProvers.var_eq_tac >> > MATCH_ACCEPT_TAC listTheory.APPEND_ASSOC);
This one works similarly, but is more explicit: prove( “(∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2)”, disch_then ((CHOOSE_THEN THEN_TCL CONJUNCTS_THEN) SUBST1_TAC) >> MATCH_ACCEPT_TAC listTheory.APPEND_ASSOC); -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan ------------------------------------------------------------------------------ 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
