(**************************************************************************)
include "basic_2/notation/functions/weight_3.ma".
-include "basic_2/grammar/genv.ma". (**) (* including genv after lenv shows a disambiguation bug: only the last interpretation is considered *)
include "basic_2/grammar/lenv_weight.ma".
-include "basic_2/grammar/cl_shift.ma".
+include "basic_2/grammar/genv.ma".
(* WEIGHT OF A CLOSURE ******************************************************)
qed.
lemma fw_lpair_sn: ∀I,G,L,V,T. ♯{G, L, V} < ♯{G, L.ⓑ{I}V, T}.
-normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *)
+normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/
qed.
(* Basic_1: removed theorems 7: