Level: Lib Thy Top: 1
Hypotheses:

  1. p :

  2. q :

Conclusion:

if p then q else q fi

Applied Tactic: (BoolCases 1 THEN Reduce 0 ...)
Generated subgoals:

None