ChopAssoc	⊢ (f0 ; f1) ; f2 ≡ f0 ; (f1 ; f2)
OrChopImp	⊢ (f0 ∨ f1) ; f2 ⊃ (f0 ; f2) ∨ (f1 ; f2)
ChopOrImp	⊢ f0 ; (f1 ∨ f2) ⊃ (f0 ; f1) ∨ (f0 ; f2)
EmptyChop	⊢ empty ; f ≡ f
ChopEmpty	⊢ f ; empty ≡ f
BiBoxChopImpChop	⊢ (f0 ⊃ f1) ∧ (f2 ⊃ f3) ⊃ (f0 ; f2) ⊃ (f1 ; f3)
StateImpBi	⊢ w ⊃ w
NextImpNotNextNot	⊢ f ⊃ ¬¬f
BoxInduct	⊢ f ∧ (f ⊃ f) ⊃ f
InfChop	⊢ (f ∧ inf) ; g ≡ (f ∧ inf)
ChopStarEqv	⊢ f∗≡ (empty ∨ ((f ∧ more) ; f∗))
ChopstarInduct	⊢ (inf ∧ f ∧ (f ⊃ (g ∧ fmore) ; f)) ⊃ g∗
MP	⊢ f0 ⊃ f1, ⊢ f0 ⇒ ⊢ f1
BoxGen	⊢ f0 ⇒ ⊢ f0
BiGen	⊢ f0 ⇒ ⊢ f0