From e0f467c8489ee9df84d6afa617e10f9cf64ce79d Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 24 Sep 2024 05:32:59 +0200
Subject: [PATCH] add inversion lemmas (without proof)

---
 coq/soundness/translate_expr.v | 43 +---------------------------------
 1 file changed, 1 insertion(+), 42 deletions(-)

diff --git a/coq/soundness/translate_expr.v b/coq/soundness/translate_expr.v
index 07d58ae..b6c3636 100644
--- a/coq/soundness/translate_expr.v
+++ b/coq/soundness/translate_expr.v
@@ -10,50 +10,9 @@ Require Import subst_lemmas.
 Require Import typing.
 Require Import typing_weakening.
 Require Import typing_regular.
+Require Import typing_inv.
 Require Import translate_morph.
 
-Lemma typing_inv_tabs : forall Γ t τ,
-  (Γ |- [{ Λ t }] \is [< ∀ τ >]) ->
-  forall L x, x `notin` L ->
-  (Γ |- (expr_open_type (ty_fvar x) t) \is τ)
-.
-Proof.
-Admitted.
-
-
-Lemma typing_inv_abs : forall Γ σ t τ,
-  (Γ |- [{ λ σ ↦ t }] \is [< σ -> τ >]) ->
-  forall L x, x `notin` L ->
-  ((x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)
-.
-Proof.
-Admitted.
-
-
-Lemma typing_inv_morph : forall Γ σ t τ,
-  (Γ |- [{ λ σ ↦morph t }] \is [< σ ->morph τ >]) ->
-  forall L x, x `notin` L ->
-  ((x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)
-.
-Proof.
-  intros.
-  
-  inversion H.
-  subst.
-  
-Admitted.
-
-
-Lemma typing_inv_let : forall Γ s σ t τ,
-  (Γ |- s \is σ) ->
-  (Γ |- [{ let s in t }] \is [< τ >]) ->
-  forall L x, x `notin` L ->
-  ((x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)
-.
-Proof.
-Admitted.
-
-
 
 (*
  * translated morphism path has valid typing