Add a transformation destruct*
Add a transformation that performs destruct recursively on an hypothesis. It should handle all currently handled constructs: disjunction, conjunction, implications.
predicate p1
predicate p2
predicate p3
axiom H: p1 -> p2 -> p3
goal G: 1 = 1
destruct H should produce 3 new goals for p1, p2 and H : p3 |- G ? [EDIT: To be more clear]
This should produce 3 new subgoals which are the following:
predicate p1
predicate p2
predicate p3
goal G : p1
predicate p1
predicate p2
predicate p3
goal G : p2
predicate p1
predicate p2
predicate p3
axiom H : p3
goal G : 1 = 1
Sorry for the misleading notations.