(* forward lemmas on "qrst" strongly normalizing closures *********************)
-lemma snv_fwd_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦥[h, g] ⦃G, L, T⦄.
-#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/
+lemma snv_fwd_fsb: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ⦥[h, o] ⦃G, L, T⦄.
+#h #o #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/
qed-.