Cic.term -> ProofEngineTypes.tactic
val discriminate : term:Cic.term -> ProofEngineTypes.tactic
val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic
+val elim_intros : term:Cic.term -> ProofEngineTypes.tactic
val elim_type : term:Cic.term -> ProofEngineTypes.tactic
val exact : term:Cic.term -> ProofEngineTypes.tactic
val exists : ProofEngineTypes.tactic