proposition: Lemma SubSem_RcS {Γ Γ' Γ''} (r : Ren Γ' Γ'') (s : Sub Γ Γ') (se : SemEnv Γ) : SubSem (RcS r s) se = RenSem r (SubSem s se).
proof: Proof. generalize dependent Γ. induction r; intros; simpl; simp RcS; simp RenSem; auto; dependent elimination s; simp RcS; simp SubSem; simp RenSem. now rewrite IHr. 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)