-inductive drops (c:bool): rtmap → relation lenv ≝
-| drops_atom: ∀f. (c = Ⓣ → 𝐈⦃f⦄) → drops c (f) (⋆) (⋆)
-| drops_drop: ∀I,L1,L2,V,f. drops c f L1 L2 → drops c (⫯f) (L1.ⓑ{I}V) L2
-| drops_skip: ∀I,L1,L2,V1,V2,f.
- drops c f L1 L2 → ⬆*[f] V2 ≡ V1 →
- drops c (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2)
+inductive drops (b:bool): rtmap → relation lenv ≝
+| drops_atom: ∀f. (b = Ⓣ → 𝐈⦃f⦄) → drops b (f) (⋆) (⋆)
+| drops_drop: ∀f,I,L1,L2,V. drops b f L1 L2 → drops b (⫯f) (L1.ⓑ{I}V) L2
+| drops_skip: ∀f,I,L1,L2,V1,V2.
+ drops b f L1 L2 → ⬆*[f] V2 ≡ V1 →
+ drops b (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2)