Hi，
How can I instantiate the variable which constrained by the existential
quantifier in the parentheses(i.e. (?x. _) ==> _, replacing x with a specific
value.)? For example,
(?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2)
Now I want to instantiate `l` using `[]` ,which tactic or lemma I could use(I
know I can use simplify tactics here, but that not I wanted.)? I have seen the
proof process of APPEND_EQ_APPEND, but it didn't instantiate `l`.
Regards,
Liu
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
