proposition: Lemma activeEnv_subset_arg : forall Marg M, isArg Marg M -> envSubset (activeEnv Marg) (activeEnv M).
proof: Proof. intros. apply activeEnv_subset_unit. apply appArg_is_appUnit; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)