proposition: Lemma Plug_injective {Γ τ τ'} {C : Ctxt Γ τ' τ} e : ∀ e1, Plug e1 C e → ∀ e2, Plug e2 C e → e1 = e2.
proof: Proof. intros. dependent induction H0. - now inv H. - dependent destruction H. now f_equal; auto. - dependent destruction H. now f_equal; auto. - dependent destruction H. now f_equal; auto. - dependent destruction H. now f_equal; auto. - dependent destruction H. now f_equal; auto. - dependent destruction H. now f_equal; auto. 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)