proposition: Lemma beta_lowering : forall M (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp)), env (subst (beta_subst M Mapp MLabs)) |= 0 :! .
proof: Proof. intros. rewrite beta_env. right; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)