STRUCT_CASES_TAC : thm_tactic
th = A' |- ?y11...y1m. x = t1 /\ (B11 /\ ... /\ B1k) \/ ... \/ ?yn1...ynp. x = tn /\ (Bn1 /\ ... /\ Bnp)
A ?- s =============================================================== A u {B11,...,B1k} ?- s[t1/x] ... A u {Bn1,...,Bnp} ?- s[tn/x]
# g `~(l:(A)list = []) ==> LENGTH l > 0`;;
list_CASES = !l. l = [] \/ (?h t. l = CONS h t)
# e(STRUCT_CASES_TAC (SPEC_ALL list_CASES));; val it : goalstack = 2 subgoals (2 total) `~(CONS h t = []) ==> LENGTH (CONS h t) > 0` `~([] = []) ==> LENGTH [] > 0`