+
+fact gdrop_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇓[e] G ≡ G2 → G = G1. 𝕓{I} V →
+ e < |G1| → ⇓[e] G1 ≡ G2.
+#I #G #G1 #G2 #V #e * -G -G2
+[ #G #H1 #H destruct #H2
+ lapply (le_to_lt_to_lt … H1 H2) -H1 -H2 normalize in ⊢ (? % ? → ?); >commutative_plus #H
+ lapply (lt_plus_to_lt_l … 0 H) -H #H
+ elim (lt_zero_false … H)
+| #G #H1 #H2 destruct >(injective_plus_l … H1) -H1 #H
+ elim (lt_refl_false … H)
+| #J #G #G2 #W #_ #HG2 #H destruct //
+]
+qed.
+
+lemma gdrop_inv_lt: ∀I,G1,G2,V,e.
+ ⇓[e] G1. 𝕓{I} V ≡ G2 → e < |G1| → ⇓[e] G1 ≡ G2.
+/2 width=5/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma gdrop_total: ∀e,G1. ∃G2. ⇓[e] G1 ≡ G2.
+#e #G1 elim G1 -G1 /3 width=2/
+#I #V #G1 * #G2 #HG12
+elim (lt_or_eq_or_gt e (|G1|)) #He
+[ /3 width=2/
+| destruct /3 width=2/
+| @ex_intro [2: @gdrop_gt normalize /2 width=1/ | skip ] (**) (* explicit constructor *)
+]
+qed.