fact: Fixpoint Plug_comp {Γ τ τ' τ''} {x : Exp Γ τ''} {y : Exp Γ τ'} {z : Exp Γ τ} {C : Ctxt Γ τ' τ} {C' : Ctxt Γ τ'' τ'} (P : Plug x C' y) (P' : Plug y C z) : Plug x (Ctxt_comp C C') z := match P' with | Plug_Hole _ => P | Plug_PairL _ p' => Plug_PairL _ (Plug_comp P p') | Plug_PairR _ V p' => Plug_PairR _ V (Plug_comp P p') | Plug_Fst _ p' => Plug_Fst _ (Plug_comp P p') | Plug_Snd _ p' => Plug_Snd _ (Plug_comp P p') | Plug_AppL _ p' => Plug_AppL _ (Plug_comp P p') | Plug_AppR _ V p' => Plug_AppR _ V (Plug_comp P p') end.
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)