sig val print : AAC_coq.Relation.t -> AAC_theory.Trans.ir -> (int * AAC_matcher.Terms.t * AAC_matcher.Subst.t AAC_search_monad.m) AAC_search_monad.m -> Term.rel_context -> Proof_type.tactic end