Next Prev Up
ChopImpDf

⊢ f ⌢ g ⊃ f ChopImpDf

Proof:

1
g ⊃ true
Prop
2
f ⌢ g ⊃ f ⌢ true
1,RightChopImpChop
3
f ⌢ g ⊃ f
2, def. of 

qed

Next Prev Up

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