ProofEngineTypes.apply_tactic
(EqualityTactics.rewrite_tac ~direction:`RightToLeft
~pattern:(ProofEngineTypes.conclusion_pattern None)
ProofEngineTypes.apply_tactic
(EqualityTactics.rewrite_tac ~direction:`RightToLeft
~pattern:(ProofEngineTypes.conclusion_pattern None)