proposition: Lemma Redex_deterministic {Γ τ} {e : Exp Γ τ} : ∀ e', Redex e e' → ∀ e'', Redex e e'' → e' = e''.
proof: Proof. intros. dependent induction H0; dependent elimination H; eauto. 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)