NTactics.apply_tac ("",0,mk_id "refl");
NTactics.shift_tac;
elim_tac ~what:("",0,mk_id "Hterm") ~where;
- NTactics.branch_tac] @
+ NTactics.branch_tac ~force:true] @
HExtlib.list_concat ~sep:[NTactics.shift_tac]
(List.map (fun id-> [NTactics.apply_tac ("",0,mk_id id)]) hyplist) @
[NTactics.merge_tac;