proposition: Lemma multistep_AppR {Γ dom cod} {e e' : Γ ⊢ dom} {v : Γ ⊢ (dom ⟶ cod)} : (e --->* e') → ValueP v → APP v e --->* APP v e'.
proof: Proof. intros. induction X. - now apply multi_refl. - rewrite <- IHX; clear IHX; auto. inv H. eapply (AppR_LAM (e:=e)) in r. now apply multi_R. Qed.
imports: Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Category.Instance.Lambda.Sem Category.Instance.Lambda.Step Equations(Equations)