proposition: Lemma SubSem_ScS {Γ Γ' Γ''} (s : Sub Γ' Γ'') (t : Sub Γ Γ') (se : SemEnv Γ) : SubSem (ScS s t) se = SubSem s (SubSem t se).
proof: Proof. generalize dependent Γ''. induction s; intros; simpl; simp SubSem; auto. now rewrite <- SemExp_SubSem, IHs. 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)