| ⊢ | f ≡ f | DiEqvDiDi |
Proof:
1 | ⊢ true ≡true ; true | |
2 | ⊢ f ; true ≡ f ; (true ; true) | |
3 | ⊢ (f ; true) ; true ≡ f ; (true ; true) | |
4 | ⊢ f ; true ≡ (f ; true) ; true | |
5 | ⊢ f ≡ f | 4, def. of |
qed