-inductive fsup: bi_relation lenv term ≝
-| fsup_lref_O : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
-| fsup_pair_sn : ∀I,L,V,T. fsup L (②{I}V.T) L V
-| fsup_bind_dx : ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
-| fsup_flat_dx : ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T
-| fsup_ldrop_lt: ∀L,K,T,U,d,e.
- ⇩[d, e] L ≡ K → ⇧[d, e] T ≡ U → 0 < e → fsup L U K T
-| fsup_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e.
+(* activate genv *)
+inductive fsup: tri_relation genv lenv term ≝
+| fsup_lref_O : ∀I,G,L,V. fsup G (L.ⓑ{I}V) (#0) G L V
+| fsup_pair_sn : ∀I,G,L,V,T. fsup G L (②{I}V.T) G L V
+| fsup_bind_dx : ∀a,I,G,L,V,T. fsup G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
+| fsup_flat_dx : ∀I,G,L,V,T. fsup G L (ⓕ{I}V.T) G L T
+| fsup_ldrop_lt: ∀G,L,K,T,U,d,e.
+ ⇩[d, e] L ≡ K → ⇧[d, e] T ≡ U → 0 < e → fsup G L U G K T
+| fsup_ldrop : ∀G1,G2,L1,K1,K2,T1,T2,U1,d,e.