(* Forward lemmas with length for local environments ************************)
lemma feqg_fwd_length (S) (G1) (G2) (L1) (L2) (T1) (T2):
- â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d« → |L1| = |L2|.
+ â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d© → |L1| = |L2|.
/3 width=6 by feqg_fwd_reqg_sn, reqg_fwd_length/ qed-.