proposition: Lemma AppL_LAM {Γ dom cod} {e e' : Exp Γ (dom ⟶ cod)} {x : Exp Γ dom} : e ---> e' → APP e x ---> APP e' x.
proof: Proof. intros. dependent induction H; now eauto 6. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Sub Equations(Equations)