proposition: Lemma beta_app_reduct : forall M N (Mapp: isApp M), M -b-> N -> (exists MLabs: isAbs (appBodyL Mapp), N = lower (subst (beta_subst M Mapp MLabs)) (beta_lowering M Mapp MLabs)) \/ exists Napp: isApp N, (appBodyL Mapp = appBodyL Napp /\ appBodyR Mapp -b-> appBodyR Napp) \/ (appBodyL Mapp -b-> appBodyL Napp /\ appBodyR Mapp = appBodyR Napp).
proof: Proof. intros M N Mapp MN. inversion MN; term_inv M; try_solve. left; inversion H. exists MLabs. rewrite (app_proof_irr Tr Mapp Mapp1); trivial. right; exists Napp; fo. right; exists Napp; fo. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)