proposition: Lemma SubExp_RenExp `(s : Sub [] Γ) (r' : Ren Γ []) `(e : [] ⊢ τ) : SubExp s (RenExp r' e) = e.
proof: Proof. simpl; induction s. - dependent destruction r'; simpl. rewrite !NoSub_idSub, !SubExp_idSub. now rewrite !NoRen_idRen, !RenExp_idRen. - dependent elimination r'; simpl. rewrite <- SubExp_RcS in *. simp RcS. now rewrite SubExp_RcS. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)