fact: Fixpoint liftR Γ `(e : Exp Γ' τ) : Exp (Γ ++ Γ') τ := match Γ with | [] => e | x :: xs => RenExp skip1 (liftR xs e) end.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)