-theorem drops_trans: ∀b1,f1,L1,L. ⬇*[b1, f1] L1 ≘ L →
- ∀b2,f2,L2. ⬇*[b2, f2] L ≘ L2 →
- ∀f. f1 ⊚ f2 ≘ f → ⬇*[b1∧b2, f] L1 ≘ L2.
+theorem drops_trans: ∀b1,f1,L1,L. ⬇*[b1,f1] L1 ≘ L →
+ ∀b2,f2,L2. ⬇*[b2,f2] L ≘ L2 →
+ ∀f. f1 ⊚ f2 ≘ f → ⬇*[b1∧b2,f] L1 ≘ L2.