At: assert of bor 1
1. p: 
2. q:
(p 
q) 
p q
By:
OnHyps [2;1] BoolInd
THEN
Rewrite (ORTHENC (ORTHENC (UnfoldC `bor`) (HigherC ifthenelse_evalC)) (HigherC assert_evalC))
0
Generated subgoals:| 1 | 1. True
True True |
| 2 | 1. True
False True |
| 3 | 1. True
True False |
| 4 | 1. False False
False |