fact: Definition solve_tauto : tactic := mfix0 solve_tauto : gtactic _ := assumption || exact I || (split &> solve_tauto) || (left &> solve_tauto) || (right &> solve_tauto) || (introsn_cont solve_tauto 1) || (eexists |1> solve_tauto) || raise TautoFail.
imports: Mtac2(Mtac2 Ttactics Sorts) Coq(List)