| ⊢ | f ≡if w then g else h ⇒ ⊢ f ≡if w then g else h | DiIfEqvRule |
Proof:
1 | ⊢ f ≡if w then g else h | given |
2 | ⊢ f ; true ≡if w then (g ; true) else (h ; true) | |
3 | ⊢ f ≡if w then g else h | 2, def. of |
qed