proposition: Lemma Keep_RcR Γ Γ' Γ'' τ (r : Ren Γ' Γ'') (r' : Ren Γ Γ') : Keep (τ := τ) (RcR r r') = RcR (Keep r) (Keep r').
proof: Proof. generalize dependent Γ''. now induction r'. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)