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