proposition: Lemma AppR_LAM {Γ dom cod} {e : Exp (dom :: Γ) cod} {x x' : Exp Γ dom} : x ---> x' → APP (LAM e) x ---> APP (LAM 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)