proposition: Lemma SubSem_ScR {Γ Γ' Γ''} (s : Sub Γ' Γ'') (r : Ren Γ Γ') (se : SemEnv Γ) : SubSem (ScR s r) se = SubSem s (RenSem r se).
proof: Proof. generalize dependent Γ''. generalize dependent Γ'. destruct Γ, se; simpl; intros; auto. - dependent elimination r; simp RenSem. rewrite NoRen_idRen. now rewrite ScR_idRen. - clear. dependent induction s1; simp ScR. + now simp SubSem. + simp SubSem. f_equal. * now rewrite SemExp_RenSem. * dependent elimination r; simp RenSem; now rewrite IHs1. 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)