G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)])
| IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)])
G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)])
| IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)])