Next Prev Up
ChopAndNotFin

⊢ f ; g ∧¬fin w ≡ f ; (g ∧¬fin w) ChopAndNotFin

Proof:

1
⊢ f ; g ∧fin ¬w ≡ f ; (g ∧fin ¬w)
ChopAndFin
2
⊢ fin ¬w ≡¬fin w
PTL
3
⊢ g ∧fin ¬w ≡ g ∧¬fin w
2,Prop
4
⊢ f ; (g ∧fin ¬w) ≡ f ; (g ∧¬fin w)
3,LeftChopEqvChop
5
⊢ f ; g ∧¬fin w ≡ f ; (g ∧¬fin w)
1, 2, 4,Prop

qed

Next Prev Up

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