then ProofEngineTypes.apply_tactic
(P.apply_tac
~term:(
- C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ;
+ C.Appl [(C.Const (LibraryObjects.absurd_URI , [] )) ;
term ; ty])
)
status
~start:
(EliminationTactics.elim_type_tac
~term:
- (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, [])))
+ (C.MutInd (LibraryObjects.false_URI, 0, [])))
~continuation: VariousTactics.assumption_tac))
status
with