diff --git a/coq/_CoqProject b/coq/_CoqProject
index 1c1e5b6..67c1895 100644
--- a/coq/_CoqProject
+++ b/coq/_CoqProject
@@ -17,6 +17,8 @@ typing/typing.v
 lemmas/subst_lemmas.v
 lemmas/typing_weakening.v
 lemmas/typing_regular.v
+lemmas/typing_inv.v
+lemmas/transl_inv.v
 soundness/translate_morph.v
 soundness/translate_expr.v
 
diff --git a/coq/lemmas/transl_inv.v b/coq/lemmas/transl_inv.v
new file mode 100644
index 0000000..0dc83e2
--- /dev/null
+++ b/coq/lemmas/transl_inv.v
@@ -0,0 +1,43 @@
+From Coq Require Import Lists.List.
+Require Import Atom.
+Require Import Environment.
+Require Import Metatheory.
+Require Import debruijn.
+Require Import subtype.
+Require Import env.
+Require Import morph.
+Require Import subst_lemmas.
+Require Import typing.
+
+Lemma transl_inv_let : forall Γ s s' σ t t' τ,
+  (Γ |- s \is σ) ->
+  (Γ |- [[ [{ let s in t }] \is τ ]] = [{ let s' in t' }]) ->
+  forall L x, x `notin` L ->
+  ((x, σ) :: Γ |- [[expr_open [{$ x}] t \is τ]] = expr_open [{$ x}] t')
+.
+Proof.
+Admitted.
+
+Lemma transl_inv_abs : forall Γ σ e e' τ,
+  (Γ |- [[ [{ λ σ ↦ e }] \is τ ]] = [{ λ σ ↦ e' }]) ->
+  forall L x, x `notin` L ->
+  ((x, σ) :: Γ |- [[expr_open [{$ x}] e \is τ]] = expr_open [{$ x}] e')
+.
+Proof.
+Admitted.
+
+Lemma transl_inv_morph : forall Γ σ e e' τ,
+  (Γ |- [[ [{ λ σ ↦morph e }] \is τ ]] = [{ λ σ ↦morph e' }]) ->
+  forall L x, x `notin` L ->
+  ((x, σ) :: Γ |- [[expr_open [{$ x}] e \is τ]] = expr_open [{$ x}] e')
+.
+Proof.
+Admitted.
+
+Lemma transl_inv_tabs : forall Γ e e' τ,
+  (Γ |- [[ [{ Λ e }] \is [< ∀ τ >] ]] = [{ Λ e' }]) ->
+  forall L x, x `notin` L ->
+  (Γ |- [[ (expr_open_type (ty_fvar x) e) \is τ]] = expr_open_type (ty_fvar x) e')
+.
+Proof.
+Admitted.
diff --git a/coq/lemmas/typing_inv.v b/coq/lemmas/typing_inv.v
new file mode 100644
index 0000000..90b73a7
--- /dev/null
+++ b/coq/lemmas/typing_inv.v
@@ -0,0 +1,53 @@
+From Coq Require Import Lists.List.
+Require Import Atom.
+Require Import Environment.
+Require Import Metatheory.
+Require Import debruijn.
+Require Import subtype.
+Require Import env.
+Require Import morph.
+Require Import subst_lemmas.
+Require Import typing.
+
+
+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.
+