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