Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

b1,b2:sBExpr. b1 or b2 sBExpr

Applied Tactic: Unfolds ``sbexpr sor`` 0 THEN Auto
Generated subgoals:

None