Next Prev Up
DiEqvDi

⊢ f ≡ g ⇒ ⊢ f ≡ g DiEqvDi

Proof:

1
⊢ f ≡ f1
given
2
⊢ f ; true ≡ g ; true
1,LeftChopEqvChop
3
⊢ f ≡ g
2, def. of 

qed

Here is a corollary for the operator :

Next Prev Up

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023