proposition: Lemma RenSem_RcR {Γ Γ' Γ''} (f : Ren Γ' Γ'') (g : Ren Γ Γ') (se : SemEnv Γ) : RenSem (RcR f g) se = RenSem f (RenSem g se).
proof: Proof. generalize dependent Γ''. generalize dependent Γ'. induction Γ; destruct se; simpl; intros; auto. - inversion g; subst. rewrite RenSem_inil. inversion f; subst. now rewrite !RenSem_inil. - dependent elimination g; simp RenSem. + now rewrite <- IHΓ; simp RcR; simp RenSem. + dependent elimination f; simp RenSem; now rewrite <- IHΓ; simp RcR; simp RenSem. 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)