NextImpSkipYields

⊢

f ⊃skip

NextImpSkipYields

Proof:

1	⊢ f ⊃ f	PTL
2	⊢ skip f ≡ f	SkipYieldsEqvWeakNext
3	⊢ f ⊃skip f	1, 2,Prop

qed

2024-08-03