proposition: Lemma SemExp_SubSem {Γ Γ' τ} (e : Exp Γ τ) (s : Sub Γ' Γ) (se : SemEnv Γ') : SemExp e (SubSem s se) = SemExp (SubExp s e) se.
proof: Proof. generalize dependent Γ'. induction e; simpl; intros; auto. - now rewrite IHe1, IHe2. - now rewrite IHe. - now rewrite IHe. - now rewrite SemVar_SubSem. - extensionality z. fold SemTy in z. rewrite <- IHe; clear IHe. simpl. unfold Keepₛ, Dropₛ; simp SubSem. repeat f_equal. rewrite SubSem_ScR. now rewrite RenSem_skip1. - now rewrite IHe1, IHe2. Qed.
imports: Category.Lib Category.Lib.IList Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Equations(Equations)