proposition: Theorem Ctxt_id_right {Γ τ τ'} {C : Ctxt Γ τ' τ} : Ctxt_comp C Ctxt_id = C.
proof: Proof. induction C; simpl; auto; now f_equal. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Sub Equations(Equations)