рекурсивно инвертировать гипотезы в coq

) У меня возникли проблемы с определением тактики рекурсивного обращения гипотез в контексте доказательства. Например, предположим, что я иметь контекст доказательства, содержащий такую ​​гипотезу, как:

H1 : search_tree (node a (node b ll lr) (node c rl rr))

, и хотел бы неоднократно инвертировать гипотезу, чтобы получить контекст доказательства, содержащий гипотезы

H1 : search_tree (node a (node b ll lr) (node c rl rr))
H2 : search_tree (node b ll lr)
H3 : search_tree (node c rl rr)
H4 : lt_tree a (node b ll lr)
H5 : gt_tree a (node c rl rr)
H6 : lt_tree b ll
H7 : gt_tree b lr
H8 : lt_tree c rl
H9 : gt_tree c rr

Конечно, получить этот контекст доказательства легко, многократно применяя тактику инверсии. инвертирование гипотезы поместит разные гипотезы в разные подцели, и то, нужно ли инвертировать каждую, зависит от характера информации, предоставляемой инверсией.

Очевидная проблема состоит в том, что неизбирательное сопоставление с шаблоном контекста доказательства приведет к незавершению. следующее не сработает, если кто-то хочет сохранить исходные гипотезы после их инвертирования:

Ltac invert_all :=
  match goal with
    | [ H1 : context [ node ?a ?l ?r ] |- ?goal ] => invert H1; invert_all
    | _ => idtac
  end.

Есть ли простой способ сделать это? Очевидным решением было бы сохранить стек уже в Проверенные гипотезы. Другое решение - инвертировать гипотезы только до определенной глубины, что приведет к удалению рекурсивных вызовов в Ltac.