proposition: Lemma SemExp_RenSem {Γ Γ' τ} (e : Exp Γ τ) (r : Ren Γ' Γ) (se : SemEnv Γ') : SemExp e (RenSem r se) = SemExp (RenExp r e) se.
proof: Proof. generalize dependent Γ'. induction e; simpl; intros; auto. - now rewrite IHe1, IHe2. - now rewrite IHe. - now rewrite IHe. - now rewrite SemVar_RenSem. - extensionality z. fold SemTy in z. rewrite <- IHe; clear IHe. simpl. now repeat f_equal. - 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)