Framing should succeed when a disjunct is exactly the framed hypothesis
For example, framing P
in (P ∨ Q) ∗ R
should succeed and turn the goal into R
.
In general, framing of non-persistent hypotheses in just one disjunct of a disjunction leads to information loss, so should fail. However, if framing in one disjunct turns it into True
, framing should succeed.