Type Safety using Logical Relations

Display all goals and responses

What is logical relations? That is a question we won't try to answer here in full generality. For our purposes, we can think of logical relations as a technique for proving properties about a language that can require stronger inductive hypotheses than those that are generated from inducting directly on syntax.

Instead, we will demonstrate the use of a logical relation in action on a relatively simple example, proving type safety for the simply-typed lambda calculus.

Require Import Unicode.Utf8.
Require Import Relations.Relation_Operators.
Require Import List.
Require Import Autosubst.Autosubst.

Inductive type : Type :=
| Bool
| Arr (t1 t2 : type).
Notation "S ⇒ T" := (Arr S T) (at level 80, right associativity).

Inductive term : Type :=
| TTrue
| TFalse
| TIf (e1 e2 e3: term)
| TVar (x : var)
| TLam (T : type) (e : {bind term})
| TApp (f e : term).

We use the Autosubst library to handle binding/substitutions. Here we invoke some Autosubst black magic to get all the basic lemmas about substitution for free.

#[export] Instance Ids_term : Ids term.Ids term derive. Defined.
#[export] Instance Rename_term : Rename term.Rename term derive. Defined.
#[export] Instance Subst_term : Subst term.Subst term derive. Defined.
#[export] Instance SubstLemmas_term : SubstLemmas term.SubstLemmas term derive. Qed.

Inductive value : term → Prop :=
| value_true : value TTrue
| value_false : value TFalse
| value_lam : forall T e, value (TLam T e).
#[export] Hint Constructors value : core.

Lemma value_dec : forall v, value v ∨ ¬ (value v).∀ v : term, value v ∨ ¬ value v
Proof.∀ v : term, value v ∨ ¬ value v
  destruct v; solve [auto; right; intros H; inversion H].
Qed.

Reserved Notation "e '-->' e'" (at level 80).
Inductive step : term -> term -> Prop :=
| step_beta : ∀ T e v u, value v → u = e.[v .: ids] → TApp (TLam T e) v --> u
| step_app1 : ∀ e e' e2, e --> e' → TApp e e2 --> TApp e' e2
| step_app2 : ∀ v e2 e2', value v → e2 --> e2' → TApp v e2 --> TApp v e2'
| step_if : ∀ e e' e1 e2, e --> e' → TIf e e1 e2 --> TIf e' e1 e2
| step_ifT : ∀ e1 e2, TIf TTrue e1 e2 --> e1
| step_ifF : ∀ e1 e2, TIf TFalse e1 e2 --> e2
where "e '-->' e'" := (step e e') : type_scope.
#[export] Hint Constructors step : core.

Definition multistep := clos_refl_trans_1n _ step.
Notation "e '-->*' e'" := (multistep e e') (at level 80).
#[export] Hint Constructors clos_refl_trans_1n : core.

We will need several standard lemmas about the step relation and values. I won't comment on them since they are straightforward and not the focus of this post.

Lemma multistep_step : ∀ x y, x --> y → x -->* y.∀ x y : term, x --> y → x -->* y
Proof.∀ x y : term, x --> y → x -->* y
  intros.x, y: term
H: x --> y
x -->* y econstructor; eauto.
Qed.
#[export] Hint Resolve multistep_step : core.

Lemma multistep_trans : ∀ x y z, x -->* y → y -->* z → x -->* z.∀ x y z : term, x -->* y → y -->* z → x -->* z
Proof.∀ x y z : term, x -->* y → y -->* z → x -->* z
  intros x y z H.x, y, z: term
H: x -->* y
y -->* z → x -->* z
  induction H; intros; auto.z, x, y, z0: term
H: x --> y
H0: clos_refl_trans_1n term step y z0
IHclos_refl_trans_1n: z0 -->* z → y -->* z
H1: z0 -->* z
x -->* z
  econstructor.z, x, y, z0: term
H: x --> y
H0: clos_refl_trans_1n term step y z0
IHclos_refl_trans_1n: z0 -->* z → y -->* z
H1: z0 -->* z
x --> ?y
z, x, y, z0: term
H: x --> y
H0: clos_refl_trans_1n term step y z0
IHclos_refl_trans_1n: z0 -->* z → y -->* z
H1: z0 -->* z
clos_refl_trans_1n term step ?y z apply H.z, x, y, z0: term
H: x --> y
H0: clos_refl_trans_1n term step y z0
IHclos_refl_trans_1n: z0 -->* z → y -->* z
H1: z0 -->* z
clos_refl_trans_1n term step y z apply IHclos_refl_trans_1n; auto.
Qed.

Lemma if_cond_cong : ∀ e1 e2 e3 e1', e1 -->* e1' → TIf e1 e2 e3 -->* TIf e1' e2 e3.∀ e1 e2 e3 e1' : term,
  e1 -->* e1' → TIf e1 e2 e3 -->* TIf e1' e2 e3
Proof.∀ e1 e2 e3 e1' : term,
  e1 -->* e1' → TIf e1 e2 e3 -->* TIf e1' e2 e3
  intros ? ? ? ? H.e1, e2, e3, e1': term
H: e1 -->* e1'
TIf e1 e2 e3 -->* TIf e1' e2 e3
  induction H; auto; [constructor |].e2, e3, x, y, z: term
H: x --> y
H0: clos_refl_trans_1n term step y z
IHclos_refl_trans_1n: TIf y e2 e3 -->* TIf z e2 e3
TIf x e2 e3 -->* TIf z e2 e3
  econstructor; [constructor; apply H | auto].
Qed.

Lemma app_cong1 : ∀ e1 e2 e1', e1 -->* e1' → TApp e1 e2 -->* TApp e1' e2.∀ e1 e2 e1' : term,
  e1 -->* e1' → TApp e1 e2 -->* TApp e1' e2
Proof.∀ e1 e2 e1' : term,
  e1 -->* e1' → TApp e1 e2 -->* TApp e1' e2
  intros ? ? ? H.e1, e2, e1': term
H: e1 -->* e1'
TApp e1 e2 -->* TApp e1' e2
  induction H; [constructor |].e2, x, y, z: term
H: x --> y
H0: clos_refl_trans_1n term step y z
IHclos_refl_trans_1n: TApp y e2 -->* TApp z e2
TApp x e2 -->* TApp z e2
  econstructor; [constructor; apply H | auto].
Qed.

Lemma app_cong2 : ∀ τ e1 e2 e2', e2 -->* e2' → TApp (TLam τ e1) e2 -->* TApp (TLam τ e1) e2'.∀ (τ : type) (e1 : {bind term}) (e2 e2' : term),
  e2 -->* e2'
  → TApp (TLam τ e1) e2 -->* TApp (TLam τ e1) e2'
Proof.∀ (τ : type) (e1 : {bind term}) (e2 e2' : term),
  e2 -->* e2'
  → TApp (TLam τ e1) e2 -->* TApp (TLam τ e1) e2'
  intros ? ? ? ? H.τ: type
e1: {bind term}
e2, e2': term
H: e2 -->* e2'
TApp (TLam τ e1) e2 -->* TApp (TLam τ e1) e2'
  induction H; [constructor |].τ: type
e1: {bind term}
x, y, z: term
H: x --> y
H0: clos_refl_trans_1n term step y z
IHclos_refl_trans_1n: TApp (TLam τ e1) y -->*
TApp (TLam τ e1) z
TApp (TLam τ e1) x -->* TApp (TLam τ e1) z
  econstructor; [apply step_app2; [constructor | apply H] | auto].
Qed.

Definition nf (t : term) := ∀ t', ¬ (t --> t').
Lemma value_is_nf : ∀ v, value v → nf v.∀ v : term, value v → nf v
Proof.∀ v : term, value v → nf v
  intros v Hv.v: term
Hv: value v
nf v
  destruct Hv; intros t' Hstep; inversion Hstep.
Qed.
Ltac value_step :=
  match goal with
  | [ Hv : TLam ?T ?e --> _ |- _ ] => inversion Hv
  | [ Hv : TTrue --> _ |- _ ] => inversion Hv
  | [ Hv : TFalse --> _ |- _ ] => inversion Hv
  | [ Hv : value ?v, Hstep : ?v --> ?e  |- _ ] => exfalso; apply (value_is_nf _ Hv _ Hstep)
  end.

Lemma value_multistep : ∀ {v v'}, value v → v -->* v' → v' = v.∀ v v' : term, value v → v -->* v' → v' = v
Proof.∀ v v' : term, value v → v -->* v' → v' = v
  intros v v' H1 H2.v, v': term
H1: value v
H2: v -->* v'
v' = v
  inversion H2; [auto | value_step].
Qed.

Definition irred (e : term) := forall e', ¬ (e --> e').
Ltac irred_step :=
  match goal with
  | [ H : irred ?e, Hstep : ?e --> ?e' |- _ ] => exfalso; apply H in Hstep; assumption
  end.

Lemma irred_dec : ∀ e, (∃ e', e --> e') ∨ irred e.∀ e : term, (∃ e' : term, e --> e') ∨ irred e
Proof.∀ e : term, (∃ e' : term, e --> e') ∨ irred e
  induction e; try solve [right; intros ? H; inversion H; value_step].e1, e2, e3: term
IHe1: (∃ e' : term, e1 --> e') ∨ irred e1
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
IHe3: (∃ e' : term, e3 --> e') ∨ irred e3
(∃ e' : term, TIf e1 e2 e3 --> e')
∨ irred (TIf e1 e2 e3)
e1, e2: term
IHe1: (∃ e' : term, e1 --> e') ∨ irred e1
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
  -e1, e2, e3: term
IHe1: (∃ e' : term, e1 --> e') ∨ irred e1
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
IHe3: (∃ e' : term, e3 --> e') ∨ irred e3
(∃ e' : term, TIf e1 e2 e3 --> e')
∨ irred (TIf e1 e2 e3) destruct e1; try solve [left; eexists; auto];
      repeat (destruct IHe1 as [[e1' ?] | ?]; [
            left; eexists; apply step_if; apply H |
      right; intros e' Hstep; inversion Hstep; subst; irred_step ]).
  -e1, e2: term
IHe1: (∃ e' : term, e1 --> e') ∨ irred e1
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2) destruct IHe1 as [[e1' ?] | ?].e1, e2, e1': term
H: e1 --> e1'
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
e1, e2: term
H: irred e1
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
    left.e1, e2, e1': term
H: e1 --> e1'
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
∃ e' : term, TApp e1 e2 --> e'
e1, e2: term
H: irred e1
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2) eexists.e1, e2, e1': term
H: e1 --> e1'
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
TApp e1 e2 --> ?e'
e1, e2: term
H: irred e1
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2) constructor.e1, e2, e1': term
H: e1 --> e1'
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
e1 --> ?e'
e1, e2: term
H: irred e1
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2) apply H.e1, e2: term
H: irred e1
IHe2: (∃ e' : term, e2 --> e') ∨ irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
    destruct IHe2 as [[e2' ?] | ?].e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
e1, e2: term
H: irred e1
H0: irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
    destruct (value_dec e1).e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: value e1
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
e1, e2: term
H: irred e1
H0: irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
    *e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: value e1
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2) left.e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: value e1
∃ e' : term, TApp e1 e2 --> e' eexists.e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: value e1
TApp e1 e2 --> ?e' apply step_app2.e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: value e1
value e1
e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: value e1
e2 --> ?e2' apply H1.e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: value e1
e2 --> ?e2' apply H0.
    *e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2) right.e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
irred (TApp e1 e2) intros e' Hstep.e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
e': term
Hstep: TApp e1 e2 --> e'
False inversion Hstep; subst.e2, e: term
T: type
Hstep: TApp (TLam T e) e2 --> e.[e2/]
H: irred (TLam T e)
e2': term
H0: e2 --> e2'
H1: ¬ value (TLam T e)
H4: value e2
False
e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
e'0: term
Hstep: TApp e1 e2 --> TApp e'0 e2
H5: e1 --> e'0
False
e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
e2'0: term
Hstep: TApp e1 e2 --> TApp e1 e2'0
H4: value e1
H6: e2 --> e2'0
False value_step.e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
e'0: term
Hstep: TApp e1 e2 --> TApp e'0 e2
H5: e1 --> e'0
False
e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
e2'0: term
Hstep: TApp e1 e2 --> TApp e1 e2'0
H4: value e1
H6: e2 --> e2'0
False irred_step.e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
e2'0: term
Hstep: TApp e1 e2 --> TApp e1 e2'0
H4: value e1
H6: e2 --> e2'0
False apply H1.e1, e2: term
H: irred e1
e2': term
H0: e2 --> e2'
H1: ¬ value e1
e2'0: term
Hstep: TApp e1 e2 --> TApp e1 e2'0
H4: value e1
H6: e2 --> e2'0
value e1 assumption.
    *e1, e2: term
H: irred e1
H0: irred e2
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2) destruct (value_dec e1).e1, e2: term
H: irred e1
H0: irred e2
H1: value e1
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
      destruct H1; try (right; intros e' Hstep; inversion Hstep; subst; irred_step).e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
(∃ e' : term, TApp (TLam T e) e2 --> e')
∨ irred (TApp (TLam T e) e2)
e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2)
    +e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
(∃ e' : term, TApp (TLam T e) e2 --> e')
∨ irred (TApp (TLam T e) e2) destruct (value_dec e2).e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: value e2
(∃ e' : term, TApp (TLam T e) e2 --> e')
∨ irred (TApp (TLam T e) e2)
e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
(∃ e' : term, TApp (TLam T e) e2 --> e')
∨ irred (TApp (TLam T e) e2)
      ++e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: value e2
(∃ e' : term, TApp (TLam T e) e2 --> e')
∨ irred (TApp (TLam T e) e2) left.e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: value e2
∃ e' : term, TApp (TLam T e) e2 --> e' exists e.[e2/].e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: value e2
TApp (TLam T e) e2 --> e.[e2/] constructor; auto.
      ++e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
(∃ e' : term, TApp (TLam T e) e2 --> e')
∨ irred (TApp (TLam T e) e2) right.e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
irred (TApp (TLam T e) e2) intros e' Hstep.e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
e': term
Hstep: TApp (TLam T e) e2 --> e'
False inversion Hstep; subst.e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
Hstep: TApp (TLam T e) e2 --> e.[e2/]
H6: value e2
False
e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
e'0: term
Hstep: TApp (TLam T e) e2 --> TApp e'0 e2
H5: TLam T e --> e'0
False
e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
e2': term
Hstep: TApp (TLam T e) e2 --> TApp (TLam T e) e2'
H4: value (TLam T e)
H6: e2 --> e2'
False auto.e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
e'0: term
Hstep: TApp (TLam T e) e2 --> TApp e'0 e2
H5: TLam T e --> e'0
False
e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
e2': term
Hstep: TApp (TLam T e) e2 --> TApp (TLam T e) e2'
H4: value (TLam T e)
H6: e2 --> e2'
False inversion H5.e2: term
T: type
e: {bind term}
H: irred (TLam T e)
H0: irred e2
H1: ¬ value e2
e2': term
Hstep: TApp (TLam T e) e2 --> TApp (TLam T e) e2'
H4: value (TLam T e)
H6: e2 --> e2'
False irred_step.
    +e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
(∃ e' : term, TApp e1 e2 --> e') ∨ irred (TApp e1 e2) right.e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
irred (TApp e1 e2) intros e' Hstep.e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
e': term
Hstep: TApp e1 e2 --> e'
False inversion Hstep; subst.e2, e: term
T: type
Hstep: TApp (TLam T e) e2 --> e.[e2/]
H: irred (TLam T e)
H0: irred e2
H1: ¬ value (TLam T e)
H4: value e2
False
e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
e'0: term
Hstep: TApp e1 e2 --> TApp e'0 e2
H5: e1 --> e'0
False
e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
e2': term
Hstep: TApp e1 e2 --> TApp e1 e2'
H4: value e1
H6: e2 --> e2'
False apply H1.e2, e: term
T: type
Hstep: TApp (TLam T e) e2 --> e.[e2/]
H: irred (TLam T e)
H0: irred e2
H1: ¬ value (TLam T e)
H4: value e2
value (TLam T e)
e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
e'0: term
Hstep: TApp e1 e2 --> TApp e'0 e2
H5: e1 --> e'0
False
e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
e2': term
Hstep: TApp e1 e2 --> TApp e1 e2'
H4: value e1
H6: e2 --> e2'
False constructor.e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
e'0: term
Hstep: TApp e1 e2 --> TApp e'0 e2
H5: e1 --> e'0
False
e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
e2': term
Hstep: TApp e1 e2 --> TApp e1 e2'
H4: value e1
H6: e2 --> e2'
False irred_step.e1, e2: term
H: irred e1
H0: irred e2
H1: ¬ value e1
e2': term
Hstep: TApp e1 e2 --> TApp e1 e2'
H4: value e1
H6: e2 --> e2'
False irred_step.
Qed.

Section Deterministic.
  Theorem step_deterministic : ∀ {s t₁ t₂ : term},
      s --> t₁ → s --> t₂ → t₁ = t₂.∀ s t₁ t₂ : term, s --> t₁ → s --> t₂ → t₁ = t₂
  Proof.∀ s t₁ t₂ : term, s --> t₁ → s --> t₂ → t₁ = t₂
    intros s t₁ t₂ Ht₁.s, t₁, t₂: term
Ht₁: s --> t₁
s --> t₂ → t₁ = t₂
    generalize dependent t₂.s, t₁: term
Ht₁: s --> t₁
∀ t₂ : term, s --> t₂ → t₁ = t₂
    induction Ht₁; intros t₂ Ht₂; inversion Ht₂; subst; auto; try value_step; solve [f_equal; apply IHHt₁; auto].
  Qed.

  Corollary confluence : ∀ {t u v : term},
      t -->* u → t -->* v → ∃ z, u -->* z ∧ v -->* z.∀ t u v : term,
  t -->* u
  → t -->* v → ∃ z : term, (u -->* z) ∧ v -->* z
  Proof.∀ t u v : term,
  t -->* u
  → t -->* v → ∃ z : term, (u -->* z) ∧ v -->* z
    intros t u v Hu.t, u, v: term
Hu: t -->* u
t -->* v → ∃ z : term, (u -->* z) ∧ v -->* z
    generalize dependent v.t, u: term
Hu: t -->* u
∀ v : term,
  t -->* v → ∃ z : term, (u -->* z) ∧ v -->* z
    induction Hu; intros v Hv.x, v: term
Hv: x -->* v
∃ z : term, (x -->* z) ∧ v -->* z
x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
v: term
Hv: x -->* v
∃ z0 : term, (z -->* z0) ∧ v -->* z0
    -x, v: term
Hv: x -->* v
∃ z : term, (x -->* z) ∧ v -->* z exists v; split; [auto | constructor].
    -x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
v: term
Hv: x -->* v
∃ z0 : term, (z -->* z0) ∧ v -->* z0 destruct Hv.x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
∃ z0 : term, (z -->* z0) ∧ x -->* z0
x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
y0, z0: term
H0: x --> y0
Hv: clos_refl_trans_1n term step y0 z0
∃ z1 : term, (z -->* z1) ∧ z0 -->* z1
      *x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
∃ z0 : term, (z -->* z0) ∧ x -->* z0 exists z.x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
(z -->* z) ∧ x -->* z split; [constructor | econstructor; [apply H | assumption]].
      *x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
y0, z0: term
H0: x --> y0
Hv: clos_refl_trans_1n term step y0 z0
∃ z1 : term, (z -->* z1) ∧ z0 -->* z1 replace y0 with y in *.x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
y0, z0: term
H0: x --> y
Hv: clos_refl_trans_1n term step y z0
∃ z1 : term, (z -->* z1) ∧ z0 -->* z1
x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
y0, z0: term
H0: x --> y0
Hv: clos_refl_trans_1n term step y0 z0
y = y0 auto.x, y, z: term
H: x --> y
Hu: clos_refl_trans_1n term step y z
IHHu: ∀ v : term,
  y -->* v
  → ∃ z0 : term, (z -->* z0) ∧ v -->* z0
y0, z0: term
H0: x --> y0
Hv: clos_refl_trans_1n term step y0 z0
y = y0
        eapply step_deterministic; [apply H | assumption].
  Qed.

  Corollary irred_unique : ∀ {a b c : term}, a -->* b → a -->* c → irred b → c -->* b.∀ a b c : term,
  a -->* b → a -->* c → irred b → c -->* b
  Proof.∀ a b c : term,
  a -->* b → a -->* c → irred b → c -->* b
    intros a b c Hab Hac Hb.a, b, c: term
Hab: a -->* b
Hac: a -->* c
Hb: irred b
c -->* b
    destruct (confluence Hab Hac) as [z [Hbz Hcz]].a, b, c: term
Hab: a -->* b
Hac: a -->* c
Hb: irred b
z: term
Hbz: b -->* z
Hcz: c -->* z
c -->* b
    inversion Hbz; subst; [auto | irred_step].
  Qed.
End Deterministic.

A typing context is just represented as a list of types, where the i'th type is the type of the i'th DeBrujin index. We define our typing judgement in the standard way as an inductive relation.

Definition context := list type.
Definition empty : context := nil.

Definition lookup : context → nat → option type := @nth_error type.

Reserved Notation "Γ '⊢' e '∈' T'" (at level 85).
Inductive has_type : context → term → type → Prop :=
| type_var : ∀ Γ x τ, lookup Γ x = Some τ → Γ ⊢ TVar x ∈ τ
| type_true : ∀ Γ, Γ ⊢ TTrue ∈ Bool
| type_false : ∀ Γ, Γ ⊢ TFalse ∈ Bool
| type_lam : ∀ Γ e τ₁ τ₂, (τ₁ :: Γ) ⊢ e ∈ τ₂ → Γ ⊢ TLam τ₁ e ∈ τ₁ ⇒ τ₂
| type_app : ∀ Γ f e τ τ₂, Γ ⊢ f ∈ τ₂ ⇒ τ → Γ ⊢ e ∈ τ₂ → Γ ⊢ TApp f e ∈ τ
| type_if : ∀ Γ e e₁ e₂ τ, Γ ⊢ e ∈ Bool → Γ ⊢ e₁ ∈ τ → Γ ⊢ e₂ ∈ τ → Γ ⊢ TIf e e₁ e₂ ∈ τ
where "Γ '⊢' e '∈' T" := (has_type Γ e T).
Notation "'⊢' e '∈' T" := (empty ⊢ e ∈ T) (at level 85).

Type Safety

A key property of the simply-typed lambda calculus is that it is type safe, i.e., if a program $e$ is well-typed according to the typing judgement given above, then $e$ will never evaluate to a "stuck" state. (Note that in the case of STLC, we can prove stronger properties (strong normalization) as well; however, this definition is general enough to apply to languages without normalization or even with nondeterministic behavior).

We can express this notion of type safety as follows:

Section TypeSafety.
Definition safe (e : term) := ∀ e', e -->* e' → value e' ∨ ∃ e'', e' --> e''.
Definition typesafety_statement := ∀ e τ, ⊢ e ∈ τ → safe e.

Traditionally, type safety is proven "syntactically" using progress and preservation lemmas:

Definition progress := ∀ e e' τ, ⊢ e ∈ τ → e --> e' → value e' ∨ ∃ e'', e' --> e''.
Definition preservation := ∀ e e' τ, ⊢ e ∈ τ → e --> e' → ⊢ e' ∈ τ.

Logical relations provides another method of proving type safety that can generalize well to other proofs (proving strong normalization, program equivalence, etc.). We define a unary logical relation on that describes (closed) programs that semantically behave like programs of a type $\tau$ . This logical relation should be contrasted with our typing judgement $\Gamma \vdash e \in \tau$ , which is a purely syntactic approach to describing when programs have a type $\tau$ . For example, the program

If True then False else (λ x . x)

semantically behaves like a program of type Bool, even though it does not have a type according to our typing rules. Thus the set of well-typed programs are a strict subset of the set of "semantically well-typed" programs. The logical relations method of proving type safety can be thought of as adding an intermediate step to the flow of the proof:

First we show that if a (closed) program $e$ has a type $\tau$ , then it is semantically well-typed, or behaves like a program of type $\tau$ (a notion we will formally define later).
Then, we show that if a program is semantically well-typed, then it is safe (i.e., does not go wrong).

Logical relation proofs are typically set up so that the second implication falls out almost immediately from the definition of being semantically well-typed. The first implication is typically called the fundamental lemma, and usually requires proving a suitable generalization to open terms to handle going under binders.

Ok, let's get to some concrete definitions and proofs now.

Fail Fixpoint sem_value (T : type) : term → Prop :=
  match T with
  | Bool => fun t => t = TTrue ∨ t = TFalse
  | τ₁ ⇒ τ₂ => fun t => ∃ e, t = TLam τ₁ e ∧ (∀ v, sem_value τ₁ v → sem_expr τ₂ e.[v/])
  end
with sem_expr (τ : type) : term → Prop :=
    fun e => ∀ e', e -->* e' → irred e' → sem_value τ e'.The command has indeed failed with message:
Recursive definition of sem_expr is ill-formed.
In environment
sem_value : type → term → Prop
sem_expr : type → term → Prop
τ : type
e : term
e' : term
m : e -->* e'
i : irred e'
Recursive call to sem_value has principal argument
equal to "τ" instead of
a subterm of "τ".
Recursive definition is:
"λ (τ : type) (e : term),
   ∀ e' : term, e -->* e' → irred e' → sem_value τ e'".
  Fail Notation "v '∈' '𝓥⟦' τ '⟧'" := (sem_value τ v) (at level 80).The command has indeed failed with message:
The reference sem_value was not found in the current
environment.
  Fail Notation "e '∈' '𝓔⟦' τ '⟧'" := (sem_expr τ e) (at level 80).The command has indeed failed with message:
The reference sem_expr was not found in the current
environment.

We define a pair of mutually recursive logical relations $\mathcal{V} \left[ \cdot \right]$ and $\mathcal{E} \left[ \cdot \right]$ , called value interpretations and expression interpretations, respectively.

$\mathcal{V} \left[ \texttt{Bool} \right]$ is the set of values that behave like a $\texttt{Bool}$ . As expected, there are two such values: $\texttt{True}$ and $\texttt{False}$ .
$\mathcal{V} \left[ \tau_1 \to \tau_2 \right]$ is the set of values that behave like a function type $\tau_1 \to \tau_2$ . These are lambda expressions with the property that, when an argument in $\mathcal{V} \left[ \tau_1 \right]$ is applied to it, produces an expression in $\mathcal{E} \left[ \tau_2 \right]$ .

It's key that these function values have this extra property associated with them. In a sense, this definition demands that the logical relation is preserved by the elimination forms (application), which is critical to generating a strong enough induction hypothesis.
$\mathcal{E} \left[ \tau \right]$ is the set of expressions that, when evaluated to an irreducible expression $e'$ , $e' \in \mathcal{V} \left[ \tau \right]$ .

Unfortunately, as shown above, Coq doesn't accept these definitions, as it's not able to see that the mutual recursion is well-founded. Instead, we can get rid of the mutual recursion altogether and define them like so:

Fixpoint sem_value (T : type) : term → Prop :=
  match T with
  | Bool => fun t => t = TTrue ∨ t = TFalse
  | τ₁ ⇒ τ₂ => fun t => ∃ e, t = TLam τ₁ e ∧ (∀ v, sem_value τ₁ v →
                                                   (∀ e', e.[v/] -->* e' → irred e' → sem_value τ₂ e'))
  end.
Definition sem_expr (τ : type) : term → Prop :=
  fun e => ∀ e', e -->* e' → irred e' → sem_value τ e'.

Lemma sem_value_arr : ∀ τ₁ τ₂ t, sem_value (τ₁ ⇒ τ₂) t = ∃ e, t = TLam τ₁ e ∧ (∀ v, sem_value τ₁ v → sem_expr τ₂ e.[v/]).∀ (τ₁ τ₂ : type) (t : term),
  sem_value (τ₁ ⇒ τ₂) t =
  (∃ e : {bind term},
     t = TLam τ₁ e
     ∧ (∀ v : term,
          sem_value τ₁ v → sem_expr τ₂ e.[v/]))
Proof.∀ (τ₁ τ₂ : type) (t : term),
  sem_value (τ₁ ⇒ τ₂) t =
  (∃ e : {bind term},
     t = TLam τ₁ e
     ∧ (∀ v : term,
          sem_value τ₁ v → sem_expr τ₂ e.[v/]))
  reflexivity.
Qed.

Notation "v '∈' '𝓥⟦' τ '⟧'" := (sem_value τ v) (at level 80).
Notation "e '∈' '𝓔⟦' τ '⟧'" := (sem_expr τ e) (at level 80).

Lemma sem_value_is_value : ∀ v τ, v ∈ 𝓥⟦ τ ⟧ → value v.∀ (v : term) (τ : type), v ∈ 𝓥⟦ τ ⟧ → value v
Proof.∀ (v : term) (τ : type), v ∈ 𝓥⟦ τ ⟧ → value v
  intros v τ H.v: term
τ: type
H: v ∈ 𝓥⟦ τ ⟧
value v
  destruct τ.v: term
H: v ∈ 𝓥⟦ Bool ⟧
value v
v: term
τ1, τ2: type
H: v ∈ 𝓥⟦ τ1 ⇒ τ2 ⟧
value v
  -v: term
H: v ∈ 𝓥⟦ Bool ⟧
value v destruct H; rewrite H; auto.
  -v: term
τ1, τ2: type
H: v ∈ 𝓥⟦ τ1 ⇒ τ2 ⟧
value v destruct H as [? [H ?]]; rewrite H; auto.
Qed.

Lemma sem_val_is_sem_expr : forall v τ, v ∈ 𝓥⟦ τ ⟧ → v ∈ 𝓔⟦ τ ⟧.∀ (v : term) (τ : type), v ∈ 𝓥⟦ τ ⟧ → v ∈ 𝓔⟦ τ ⟧
Proof.∀ (v : term) (τ : type), v ∈ 𝓥⟦ τ ⟧ → v ∈ 𝓔⟦ τ ⟧
  intros v τ H.v: term
τ: type
H: v ∈ 𝓥⟦ τ ⟧
v ∈ 𝓔⟦ τ ⟧
  destruct τ.v: term
H: v ∈ 𝓥⟦ Bool ⟧
v ∈ 𝓔⟦ Bool ⟧
v: term
τ1, τ2: type
H: v ∈ 𝓥⟦ τ1 ⇒ τ2 ⟧
v ∈ 𝓔⟦ τ1 ⇒ τ2 ⟧
  -v: term
H: v ∈ 𝓥⟦ Bool ⟧
v ∈ 𝓔⟦ Bool ⟧ destruct H; intros e' Hstep; subst; apply value_multistep in Hstep; subst; simpl; auto.
  -v: term
τ1, τ2: type
H: v ∈ 𝓥⟦ τ1 ⇒ τ2 ⟧
v ∈ 𝓔⟦ τ1 ⇒ τ2 ⟧ destruct H as [e [? ?]].v: term
τ1, τ2: type
e: {bind term}
H: v = TLam τ1 e
H0: ∀ v : term,
  v ∈ 𝓥⟦ τ1 ⟧
  → ∀ e' : term,
      e.[v/] -->* e' → irred e' → e' ∈ 𝓥⟦ τ2 ⟧
v ∈ 𝓔⟦ τ1 ⇒ τ2 ⟧
    subst.τ1, τ2: type
e: {bind term}
H0: ∀ v : term,
  v ∈ 𝓥⟦ τ1 ⟧
  → ∀ e' : term,
      e.[v/] -->* e' → irred e' → e' ∈ 𝓥⟦ τ2 ⟧
TLam τ1 e ∈ 𝓔⟦ τ1 ⇒ τ2 ⟧
    intros e' Hstep.τ1, τ2: type
e: {bind term}
H0: ∀ v : term,
  v ∈ 𝓥⟦ τ1 ⟧
  → ∀ e' : term,
      e.[v/] -->* e' → irred e' → e' ∈ 𝓥⟦ τ2 ⟧
e': term
Hstep: TLam τ1 e -->* e'
irred e' → e' ∈ 𝓥⟦ τ1 ⇒ τ2 ⟧ apply value_multistep in Hstep; subst; simpl; auto.τ1, τ2: type
e: {bind term}
H0: ∀ v : term,
  v ∈ 𝓥⟦ τ1 ⟧
  → ∀ e' : term,
      e.[v/] -->* e' → irred e' → e' ∈ 𝓥⟦ τ2 ⟧
irred (TLam τ1 e)
→ ∃ e0 : term,
    TLam τ1 e = TLam τ1 e0
    ∧ (∀ v : term,
         v ∈ 𝓥⟦ τ1 ⟧
         → ∀ e' : term,
             e0.[v/] -->* e' → irred e' → e' ∈ 𝓥⟦ τ2 ⟧)
    eexists; split; auto.
Qed.

A substitution is just a function from variables to expressions. A valid substitution is inductively defined with respect to a context Γ in the natural way (γ is valid if it maps all variables in Γ to semantic values).

Inductive valid_subst : context → (var → term) → Prop :=
| subst_empty : valid_subst empty ids
| subst_cons : ∀ Γ γ v τ, valid_subst Γ γ → v ∈ 𝓥⟦ τ ⟧ → valid_subst (τ :: Γ) (v .: γ).
#[local] Hint Constructors valid_subst : core.

Lemma valid_subst_var : ∀ Γ γ,
    valid_subst Γ γ → ∀ x τ, lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧.∀ (Γ : context) (γ : var → term),
  valid_subst Γ γ
  → ∀ (x : nat) (τ : type),
      lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
Proof.∀ (Γ : context) (γ : var → term),
  valid_subst Γ γ
  → ∀ (x : nat) (τ : type),
      lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
  intros Γ γ H.Γ: context
γ: var → term
H: valid_subst Γ γ
∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
  induction H; intros.x: nat
τ: type
H: lookup empty x = Some τ
ids x ∈ 𝓥⟦ τ ⟧
Γ: context
γ: var → term
v: term
τ: type
H: valid_subst Γ γ
H0: v ∈ 𝓥⟦ τ ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
x: nat
τ0: type
H1: lookup (τ :: Γ) x = Some τ0
(v .: γ) x ∈ 𝓥⟦ τ0 ⟧
  -x: nat
τ: type
H: lookup empty x = Some τ
ids x ∈ 𝓥⟦ τ ⟧ destruct x; simpl in *; discriminate.
  -Γ: context
γ: var → term
v: term
τ: type
H: valid_subst Γ γ
H0: v ∈ 𝓥⟦ τ ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
x: nat
τ0: type
H1: lookup (τ :: Γ) x = Some τ0
(v .: γ) x ∈ 𝓥⟦ τ0 ⟧ induction x.Γ: context
γ: var → term
v: term
τ: type
H: valid_subst Γ γ
H0: v ∈ 𝓥⟦ τ ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
τ0: type
H1: lookup (τ :: Γ) 0 = Some τ0
(v .: γ) 0 ∈ 𝓥⟦ τ0 ⟧
Γ: context
γ: var → term
v: term
τ: type
H: valid_subst Γ γ
H0: v ∈ 𝓥⟦ τ ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
x: nat
τ0: type
H1: lookup (τ :: Γ) (S x) = Some τ0
IHx: lookup (τ :: Γ) x = Some τ0
→ (v .: γ) x ∈ 𝓥⟦ τ0 ⟧
(v .: γ) (S x) ∈ 𝓥⟦ τ0 ⟧ inversion H1.Γ: context
γ: var → term
v: term
τ: type
H: valid_subst Γ γ
H0: v ∈ 𝓥⟦ τ ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
τ0: type
H1: lookup (τ :: Γ) 0 = Some τ0
H3: τ = τ0
(v .: γ) 0 ∈ 𝓥⟦ τ0 ⟧
Γ: context
γ: var → term
v: term
τ: type
H: valid_subst Γ γ
H0: v ∈ 𝓥⟦ τ ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
x: nat
τ0: type
H1: lookup (τ :: Γ) (S x) = Some τ0
IHx: lookup (τ :: Γ) x = Some τ0
→ (v .: γ) x ∈ 𝓥⟦ τ0 ⟧
(v .: γ) (S x) ∈ 𝓥⟦ τ0 ⟧ subst.Γ: context
γ: var → term
v: term
H: valid_subst Γ γ
τ0: type
H1: lookup (τ0 :: Γ) 0 = Some τ0
H0: v ∈ 𝓥⟦ τ0 ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
(v .: γ) 0 ∈ 𝓥⟦ τ0 ⟧
Γ: context
γ: var → term
v: term
τ: type
H: valid_subst Γ γ
H0: v ∈ 𝓥⟦ τ ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
x: nat
τ0: type
H1: lookup (τ :: Γ) (S x) = Some τ0
IHx: lookup (τ :: Γ) x = Some τ0
→ (v .: γ) x ∈ 𝓥⟦ τ0 ⟧
(v .: γ) (S x) ∈ 𝓥⟦ τ0 ⟧ assumption.Γ: context
γ: var → term
v: term
τ: type
H: valid_subst Γ γ
H0: v ∈ 𝓥⟦ τ ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
x: nat
τ0: type
H1: lookup (τ :: Γ) (S x) = Some τ0
IHx: lookup (τ :: Γ) x = Some τ0
→ (v .: γ) x ∈ 𝓥⟦ τ0 ⟧
(v .: γ) (S x) ∈ 𝓥⟦ τ0 ⟧
    apply IHvalid_subst.Γ: context
γ: var → term
v: term
τ: type
H: valid_subst Γ γ
H0: v ∈ 𝓥⟦ τ ⟧
IHvalid_subst: ∀ (x : nat) (τ : type),
  lookup Γ x = Some τ → γ x ∈ 𝓥⟦ τ ⟧
x: nat
τ0: type
H1: lookup (τ :: Γ) (S x) = Some τ0
IHx: lookup (τ :: Γ) x = Some τ0
→ (v .: γ) x ∈ 𝓥⟦ τ0 ⟧
lookup Γ x = Some τ0 assumption.
Qed.

Finally, a (possibly open) term $e$ is semantically well typed if for any valid substitution $\gamma$ , we have $\gamma(t) \in \mathcal{E} \left[ \tau \right]$ .

Definition sem_has_type (Γ : context) (e : term) (τ : type) :=
  ∀ (γ : var → term), valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ ⟧.
Notation "Γ '⊧' e '∈' τ" := (sem_has_type Γ e τ) (at level 80).
Notation "'⊧' e '∈' T" := (empty ⊧ e ∈ T) (at level 85).

Thus, our "fundamental lemma" can be stated as follows:

Definition fundlemma_statement := ∀ e τ, ⊢ e ∈ τ → ⊧ e ∈ τ.

Assuming this, type safety will follow easily:

Lemma sem_type_implies_safe : ∀ e τ, ⊧ e ∈ τ → safe e.∀ (e : term) (τ : type), ⊧ e ∈ τ → safe e
Proof.∀ (e : term) (τ : type), ⊧ e ∈ τ → safe e
  intros e τ H.e: term
τ: type
H: ⊧ e ∈ τ
safe e
  unfold sem_has_type in H.e: term
τ: type
H: ∀ γ : var → term,
  valid_subst empty γ → e.[γ] ∈ 𝓔⟦ τ ⟧
safe e
  intros e' He'.e: term
τ: type
H: ∀ γ : var → term,
  valid_subst empty γ → e.[γ] ∈ 𝓔⟦ τ ⟧
e': term
He': e -->* e'
value e' ∨ (∃ e'' : term, e' --> e'')
  destruct (irred_dec e').e: term
τ: type
H: ∀ γ : var → term,
  valid_subst empty γ → e.[γ] ∈ 𝓔⟦ τ ⟧
e': term
He': e -->* e'
H0: ∃ e'0 : term, e' --> e'0
value e' ∨ (∃ e'' : term, e' --> e'')
e: term
τ: type
H: ∀ γ : var → term,
  valid_subst empty γ → e.[γ] ∈ 𝓔⟦ τ ⟧
e': term
He': e -->* e'
H0: irred e'
value e' ∨ (∃ e'' : term, e' --> e'')
  -e: term
τ: type
H: ∀ γ : var → term,
  valid_subst empty γ → e.[γ] ∈ 𝓔⟦ τ ⟧
e': term
He': e -->* e'
H0: ∃ e'0 : term, e' --> e'0
value e' ∨ (∃ e'' : term, e' --> e'') right.e: term
τ: type
H: ∀ γ : var → term,
  valid_subst empty γ → e.[γ] ∈ 𝓔⟦ τ ⟧
e': term
He': e -->* e'
H0: ∃ e'0 : term, e' --> e'0
∃ e'' : term, e' --> e'' assumption.
  -e: term
τ: type
H: ∀ γ : var → term,
  valid_subst empty γ → e.[γ] ∈ 𝓔⟦ τ ⟧
e': term
He': e -->* e'
H0: irred e'
value e' ∨ (∃ e'' : term, e' --> e'') left.e: term
τ: type
H: ∀ γ : var → term,
  valid_subst empty γ → e.[γ] ∈ 𝓔⟦ τ ⟧
e': term
He': e -->* e'
H0: irred e'
value e' apply sem_value_is_value with τ.e: term
τ: type
H: ∀ γ : var → term,
  valid_subst empty γ → e.[γ] ∈ 𝓔⟦ τ ⟧
e': term
He': e -->* e'
H0: irred e'
e' ∈ 𝓥⟦ τ ⟧
    apply H with ids; [| rewrite subst_id |]; auto.
Qed.

The Fundamental Lemma

We need a series of lemmas that state that if an elimination form terminates, then its subexpressions must necessarily terminate as well. This clearly relies on the determinism of the step relation. The induction hypothesis is tricky; inducting on the multistep relation doesn't seem to work, since we are inducting over a relation containing a constructed term (see here). Instead we write it using a fixpoint, but we need to be careful to ensure the recursion is well founded. (Feel free to skip straight to the fundamental lemma the first time reading.)

Fixpoint tif_lemma (e' e2 e3 : term) (H : irred e') (e1 : term) (Hif : TIf e1 e2 e3 -->* e') : ∃ e1', e1 -->* e1' ∧ irred e1'.tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e', e2, e3: term
H: irred e'
e1: term
Hif: TIf e1 e2 e3 -->* e'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
Proof.tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e', e2, e3: term
H: irred e'
e1: term
Hif: TIf e1 e2 e3 -->* e'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
  destruct Hif.tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, e1: term
H: irred (TIf e1 e2 e3)
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, z: term
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
  -tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, e1: term
H: irred (TIf e1 e2 e3)
∃ e1' : term, (e1 -->* e1') ∧ irred e1' exists e1.tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, e1: term
H: irred (TIf e1 e2 e3)
(e1 -->* e1) ∧ irred e1 split.tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, e1: term
H: irred (TIf e1 e2 e3)
e1 -->* e1
tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, e1: term
H: irred (TIf e1 e2 e3)
irred e1 constructor.tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, e1: term
H: irred (TIf e1 e2 e3)
irred e1
    intros e1' Hstep.tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, e1: term
H: irred (TIf e1 e2 e3)
e1': term
Hstep: e1 --> e1'
False
    unfold irred in H.tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, e1: term
H: ∀ e' : term, ¬ (TIf e1 e2 e3 --> e')
e1': term
Hstep: e1 --> e1'
False specialize H with (TIf e1' e2 e3).tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, e1, e1': term
H: ¬ (TIf e1 e2 e3 --> TIf e1' e2 e3)
Hstep: e1 --> e1'
False auto using H.
  -tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, z: term
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
∃ e1' : term, (e1 -->* e1') ∧ irred e1' destruct (irred_dec e1).tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, z: term
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: ∃ e' : term, e1 --> e'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, z: term
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: irred e1
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
    *tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, z: term
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: ∃ e' : term, e1 --> e'
∃ e1' : term, (e1 -->* e1') ∧ irred e1' destruct H1 as [e1' H1].tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, z: term
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
e1': term
H1: e1 --> e1'
∃ e1' : term, (e1 -->* e1') ∧ irred e1' specialize tif_lemma with z e2 e3 e1'.e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
      apply tif_lemma in H.e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
H: ∃ e1'0 : term, (e1' -->* e1'0) ∧ irred e1'0
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TIf e1' e2 e3 -->* z
      destruct H as [e1'' [? ?]].e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1'': term
H: e1' -->* e1''
H2: irred e1''
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TIf e1' e2 e3 -->* z
      exists e1''.e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1'': term
H: e1' -->* e1''
H2: irred e1''
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
(e1 -->* e1'') ∧ irred e1''
e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TIf e1' e2 e3 -->* z split; [| auto].e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1'': term
H: e1' -->* e1''
H2: irred e1''
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
e1 -->* e1''
e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TIf e1' e2 e3 -->* z
      econstructor; [apply H1 | ]; auto.e2, e3, z, e1': term
tif_lemma: irred z
→ TIf e1' e2 e3 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TIf e1' e2 e3 -->* z
      replace y with (TIf e1' e2 e3) in *; [ | apply (@step_deterministic (TIf e1 e2 e3))]; auto.
    *tif_lemma: ∀ e' e2 e3 : term,
  irred e'
  → ∀ e1 : term,
      TIf e1 e2 e3 -->* e'
      → ∃ e1' : term,
          (e1 -->* e1') ∧ irred e1'
e2, e3, z: term
H: irred z
e1, y: term
H0: TIf e1 e2 e3 --> y
Hif: clos_refl_trans_1n term step y z
H1: irred e1
∃ e1' : term, (e1 -->* e1') ∧ irred e1' exists e1; split; [constructor | auto].
Qed.

Fixpoint app_lemma1 {e1 e2 e' : term} (He' : irred e') (H : TApp e1 e2 -->* e') : ∃ e1', e1 -->* e1' ∧ irred e1'.app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, e': term
He': irred e'
H: TApp e1 e2 -->* e'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
Proof.app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, e': term
He': irred e'
H: TApp e1 e2 -->* e'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
  destruct H.app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2: term
He': irred (TApp e1 e2)
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, z: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
  -app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2: term
He': irred (TApp e1 e2)
∃ e1' : term, (e1 -->* e1') ∧ irred e1' exists e1.app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2: term
He': irred (TApp e1 e2)
(e1 -->* e1) ∧ irred e1 split.app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2: term
He': irred (TApp e1 e2)
e1 -->* e1
app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2: term
He': irred (TApp e1 e2)
irred e1 constructor.app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2: term
He': irred (TApp e1 e2)
irred e1
    intros e1' Hstep.app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2: term
He': irred (TApp e1 e2)
e1': term
Hstep: e1 --> e1'
False
    unfold irred in He'.app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2: term
He': ∀ e' : term, ¬ (TApp e1 e2 --> e')
e1': term
Hstep: e1 --> e1'
False specialize He' with (TApp e1' e2).app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, e1': term
He': ¬ (TApp e1 e2 --> TApp e1' e2)
Hstep: e1 --> e1'
False auto.
  -app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, z: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
∃ e1' : term, (e1 -->* e1') ∧ irred e1' destruct (irred_dec e1).app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, z: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: ∃ e' : term, e1 --> e'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, z: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: irred e1
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
    *app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, z: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: ∃ e' : term, e1 --> e'
∃ e1' : term, (e1 -->* e1') ∧ irred e1' destruct H1 as [e1' H1].app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, z: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
e1': term
H1: e1 --> e1'
∃ e1' : term, (e1 -->* e1') ∧ irred e1' specialize app_lemma1 with e1' e2 z.e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
      apply app_lemma1 in He'.e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1: term
He': ∃ e1'0 : term, (e1' -->* e1'0) ∧ irred e1'0
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TApp e1' e2 -->* z
      destruct He' as [e1'' [? ?]].e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1, e1'': term
H2: e1' -->* e1''
H3: irred e1''
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
∃ e1' : term, (e1 -->* e1') ∧ irred e1'
e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TApp e1' e2 -->* z
      exists e1''.e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1, e1'': term
H2: e1' -->* e1''
H3: irred e1''
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
(e1 -->* e1'') ∧ irred e1''
e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TApp e1' e2 -->* z split; auto.e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1, e1'': term
H2: e1' -->* e1''
H3: irred e1''
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
e1 -->* e1''
e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TApp e1' e2 -->* z
      econstructor; [apply H1 |]; auto.e2, z, e1': term
app_lemma1: irred z
→ TApp e1' e2 -->* z
  → ∃ e1'0 : term,
      (e1' -->* e1'0) ∧ irred e1'0
e1: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e1 --> e1'
TApp e1' e2 -->* z
      replace y with (TApp e1' e2) in *; [ | apply (@step_deterministic (TApp e1 e2))]; auto.
    *app_lemma1: ∀ e1 e2 e' : term,
  irred e'
  → TApp e1 e2 -->* e'
    → ∃ e1' : term,
        (e1 -->* e1') ∧ irred e1'
e1, e2, z: term
He': irred z
y: term
H: TApp e1 e2 --> y
H0: clos_refl_trans_1n term step y z
H1: irred e1
∃ e1' : term, (e1 -->* e1') ∧ irred e1' exists e1; split; [constructor | auto].
Qed.

Fixpoint app_lemma2 {τ} {e e2 e' : term} (He' : irred e') (H : TApp (TLam τ e) e2 -->* e') : ∃ e2', e2 -->* e2' ∧ irred e2'.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, e': term
He': irred e'
H: TApp (TLam τ e) e2 -->* e'
∃ e2' : term, (e2 -->* e2') ∧ irred e2'
Proof.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, e': term
He': irred e'
H: TApp (TLam τ e) e2 -->* e'
∃ e2' : term, (e2 -->* e2') ∧ irred e2'
  destruct H.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2: term
He': irred (TApp (TLam τ e) e2)
∃ e2' : term, (e2 -->* e2') ∧ irred e2'
app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
∃ e2' : term, (e2 -->* e2') ∧ irred e2'
  -app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2: term
He': irred (TApp (TLam τ e) e2)
∃ e2' : term, (e2 -->* e2') ∧ irred e2' exists e2.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2: term
He': irred (TApp (TLam τ e) e2)
(e2 -->* e2) ∧ irred e2 split.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2: term
He': irred (TApp (TLam τ e) e2)
e2 -->* e2
app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2: term
He': irred (TApp (TLam τ e) e2)
irred e2 constructor.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2: term
He': irred (TApp (TLam τ e) e2)
irred e2
    intros e2' Hstep.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2: term
He': irred (TApp (TLam τ e) e2)
e2': term
Hstep: e2 --> e2'
False
    unfold irred in He'.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2: term
He': ∀ e' : term, ¬ (TApp (TLam τ e) e2 --> e')
e2': term
Hstep: e2 --> e2'
False specialize He' with (TApp (TLam τ e) e2').app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, e2': term
He': ¬ (TApp (TLam τ e) e2 --> TApp (TLam τ e) e2')
Hstep: e2 --> e2'
False auto.
  -app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
∃ e2' : term, (e2 -->* e2') ∧ irred e2' destruct (irred_dec e2).app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: ∃ e' : term, e2 --> e'
∃ e2' : term, (e2 -->* e2') ∧ irred e2'
app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: irred e2
∃ e2' : term, (e2 -->* e2') ∧ irred e2'
    *app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: ∃ e' : term, e2 --> e'
∃ e2' : term, (e2 -->* e2') ∧ irred e2' destruct H1 as [e2' H1].app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
e2': term
H1: e2 --> e2'
∃ e2' : term, (e2 -->* e2') ∧ irred e2' specialize app_lemma2 with τ e e2' z.τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
∃ e2' : term, (e2 -->* e2') ∧ irred e2'
      apply app_lemma2 in He'.τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2: term
He': ∃ e2'0 : term, (e2' -->* e2'0) ∧ irred e2'0
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
∃ e2' : term, (e2 -->* e2') ∧ irred e2'
τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
TApp (TLam τ e) e2' -->* z
      destruct He' as [e2'' [? ?]].τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2, e2'': term
H2: e2' -->* e2''
H3: irred e2''
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
∃ e2' : term, (e2 -->* e2') ∧ irred e2'
τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
TApp (TLam τ e) e2' -->* z
      exists e2''.τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2, e2'': term
H2: e2' -->* e2''
H3: irred e2''
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
(e2 -->* e2'') ∧ irred e2''
τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
TApp (TLam τ e) e2' -->* z split; auto.τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2, e2'': term
H2: e2' -->* e2''
H3: irred e2''
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
e2 -->* e2''
τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
TApp (TLam τ e) e2' -->* z
    +τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2, e2'': term
H2: e2' -->* e2''
H3: irred e2''
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
e2 -->* e2'' econstructor.τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2, e2'': term
H2: e2' -->* e2''
H3: irred e2''
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
e2 --> ?y
τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2, e2'': term
H2: e2' -->* e2''
H3: irred e2''
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
clos_refl_trans_1n term step ?y e2'' apply H1.τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2, e2'': term
H2: e2' -->* e2''
H3: irred e2''
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
clos_refl_trans_1n term step e2' e2'' assumption.
    +τ: type
e, z, e2': term
app_lemma2: irred z
→ TApp (TLam τ e) e2' -->* z
  → ∃ e2'0 : term,
      (e2' -->* e2'0) ∧ irred e2'0
e2: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: e2 --> e2'
TApp (TLam τ e) e2' -->* z replace y with (TApp (TLam τ e) e2') in *; [ | apply (@step_deterministic (TApp (TLam τ e) e2)) ]; auto.
      *app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: irred e2
∃ e2' : term, (e2 -->* e2') ∧ irred e2' exists e2.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: irred e2
(e2 -->* e2) ∧ irred e2 split.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: irred e2
e2 -->* e2
app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: irred e2
irred e2 constructor.app_lemma2: ∀ (τ : type) (e e2 e' : term),
  irred e'
  → TApp (TLam τ e) e2 -->* e'
    → ∃ e2' : term,
        (e2 -->* e2') ∧ irred e2'
τ: type
e, e2, z: term
He': irred z
y: term
H: TApp (TLam τ e) e2 --> y
H0: clos_refl_trans_1n term step y z
H1: irred e2
irred e2 auto.
Qed.

To prove the fundamental lemma, induct on the typing derivation. The main challenges are proving the lambda and elimination forms (App/If) cases. The App/If cases are mostly symbol pushing, using the subexpression-termination lemmas stated above.

Lemma fund_lemma : ∀ e τ, ⊢ e ∈ τ → ⊧ e ∈ τ.∀ (e : term) (τ : type), ⊢ e ∈ τ → ⊧ e ∈ τ
Proof.∀ (e : term) (τ : type), ⊢ e ∈ τ → ⊧ e ∈ τ
  intros e τ He.e: term
τ: type
He: ⊢ e ∈ τ
⊧ e ∈ τ
  induction He; intros γ Hγ; simpl.Γ: context
x: nat
τ: type
H: lookup Γ x = Some τ
γ: var → term
Hγ: valid_subst Γ γ
γ x ∈ 𝓔⟦ τ ⟧
Γ: context
γ: var → term
Hγ: valid_subst Γ γ
TTrue ∈ 𝓔⟦ Bool ⟧
Γ: context
γ: var → term
Hγ: valid_subst Γ γ
TFalse ∈ 𝓔⟦ Bool ⟧
Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
IHHe: τ₁ :: Γ ⊧ e ∈ τ₂
γ: var → term
Hγ: valid_subst Γ γ
TLam τ₁ e.[up γ] ∈ 𝓔⟦ τ₁ ⇒ τ₂ ⟧
Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
IHHe1: Γ ⊧ f ∈ (τ₂ ⇒ τ)
IHHe2: Γ ⊧ e ∈ τ₂
γ: var → term
Hγ: valid_subst Γ γ
TApp f.[γ] e.[γ] ∈ 𝓔⟦ τ ⟧
Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
IHHe1: Γ ⊧ e ∈ Bool
IHHe2: Γ ⊧ e₁ ∈ τ
IHHe3: Γ ⊧ e₂ ∈ τ
γ: var → term
Hγ: valid_subst Γ γ
TIf e.[γ] e₁.[γ] e₂.[γ] ∈ 𝓔⟦ τ ⟧
  - (* Var case *)Γ: context
x: nat
τ: type
H: lookup Γ x = Some τ
γ: var → term
Hγ: valid_subst Γ γ
γ x ∈ 𝓔⟦ τ ⟧ eauto using sem_val_is_sem_expr, valid_subst_var.
  - (* True case *)Γ: context
γ: var → term
Hγ: valid_subst Γ γ
TTrue ∈ 𝓔⟦ Bool ⟧ apply sem_val_is_sem_expr; simpl; auto.
  - (* False case *)Γ: context
γ: var → term
Hγ: valid_subst Γ γ
TFalse ∈ 𝓔⟦ Bool ⟧ apply sem_val_is_sem_expr; simpl; auto.
  - (* Lambda case *)Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
IHHe: τ₁ :: Γ ⊧ e ∈ τ₂
γ: var → term
Hγ: valid_subst Γ γ
TLam τ₁ e.[up γ] ∈ 𝓔⟦ τ₁ ⇒ τ₂ ⟧ intros e' Hstep.Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
IHHe: τ₁ :: Γ ⊧ e ∈ τ₂
γ: var → term
Hγ: valid_subst Γ γ
e': term
Hstep: TLam τ₁ e.[up γ] -->* e'
irred e' → e' ∈ 𝓥⟦ τ₁ ⇒ τ₂ ⟧
    rewrite (value_multistep (value_lam _ _) Hstep).Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
IHHe: τ₁ :: Γ ⊧ e ∈ τ₂
γ: var → term
Hγ: valid_subst Γ γ
e': term
Hstep: TLam τ₁ e.[up γ] -->* e'
irred (TLam τ₁ e.[up γ])
→ TLam τ₁ e.[up γ] ∈ 𝓥⟦ τ₁ ⇒ τ₂ ⟧
    rewrite sem_value_arr.Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
IHHe: τ₁ :: Γ ⊧ e ∈ τ₂
γ: var → term
Hγ: valid_subst Γ γ
e': term
Hstep: TLam τ₁ e.[up γ] -->* e'
irred (TLam τ₁ e.[up γ])
→ ∃ e0 : {bind term},
    TLam τ₁ e.[up γ] = TLam τ₁ e0
    ∧ (∀ v : term, v ∈ 𝓥⟦ τ₁ ⟧ → e0.[v/] ∈ 𝓔⟦ τ₂ ⟧)
    eexists; split; auto.Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
IHHe: τ₁ :: Γ ⊧ e ∈ τ₂
γ: var → term
Hγ: valid_subst Γ γ
e': term
Hstep: TLam τ₁ e.[up γ] -->* e'
H: irred (TLam τ₁ e.[up γ])
∀ v : term, v ∈ 𝓥⟦ τ₁ ⟧ → e.[up γ].[v/] ∈ 𝓔⟦ τ₂ ⟧
    intros v Hv.Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
IHHe: τ₁ :: Γ ⊧ e ∈ τ₂
γ: var → term
Hγ: valid_subst Γ γ
e': term
Hstep: TLam τ₁ e.[up γ] -->* e'
H: irred (TLam τ₁ e.[up γ])
v: term
Hv: v ∈ 𝓥⟦ τ₁ ⟧
e.[up γ].[v/] ∈ 𝓔⟦ τ₂ ⟧
    unfold sem_has_type in IHHe.Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
IHHe: ∀ γ : var → term,
  valid_subst (τ₁ :: Γ) γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
γ: var → term
Hγ: valid_subst Γ γ
e': term
Hstep: TLam τ₁ e.[up γ] -->* e'
H: irred (TLam τ₁ e.[up γ])
v: term
Hv: v ∈ 𝓥⟦ τ₁ ⟧
e.[up γ].[v/] ∈ 𝓔⟦ τ₂ ⟧
    specialize IHHe with (v .: γ).Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
γ: var → term
v: term
IHHe: valid_subst (τ₁ :: Γ) (v .: γ)
→ e.[v .: γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TLam τ₁ e.[up γ] -->* e'
H: irred (TLam τ₁ e.[up γ])
Hv: v ∈ 𝓥⟦ τ₁ ⟧
e.[up γ].[v/] ∈ 𝓔⟦ τ₂ ⟧
    replace e.[up γ].[v/] with e.[v .: γ]; [| autosubst].Γ: list type
e: term
τ₁, τ₂: type
He: τ₁ :: Γ ⊢ e ∈ τ₂
γ: var → term
v: term
IHHe: valid_subst (τ₁ :: Γ) (v .: γ)
→ e.[v .: γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TLam τ₁ e.[up γ] -->* e'
H: irred (TLam τ₁ e.[up γ])
Hv: v ∈ 𝓥⟦ τ₁ ⟧
e.[v .: γ] ∈ 𝓔⟦ τ₂ ⟧
    apply IHHe; auto.

  - (* App case *)Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
IHHe1: Γ ⊧ f ∈ (τ₂ ⇒ τ)
IHHe2: Γ ⊧ e ∈ τ₂
γ: var → term
Hγ: valid_subst Γ γ
TApp f.[γ] e.[γ] ∈ 𝓔⟦ τ ⟧ unfold sem_has_type in IHHe1, IHHe2.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
IHHe1: ∀ γ : var → term,
  valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
γ: var → term
Hγ: valid_subst Γ γ
TApp f.[γ] e.[γ] ∈ 𝓔⟦ τ ⟧
    specialize IHHe1 with γ.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
TApp f.[γ] e.[γ] ∈ 𝓔⟦ τ ⟧ specialize IHHe2 with γ.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
TApp f.[γ] e.[γ] ∈ 𝓔⟦ τ ⟧
    intros e' Hstep He'.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
e' ∈ 𝓥⟦ τ ⟧
    cut (∃ e'', e'' -->* e' ∧ e'' ∈ 𝓔⟦ τ ⟧); [intros [e'' [? ?]]; auto |].Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    destruct (app_lemma1 He' Hstep) as [f' [H1 H2]].Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f': term
H1: f.[γ] -->* f'
H2: irred f'
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    assert (TApp f.[γ] e.[γ] -->* TApp f' e.[γ]).Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f': term
H1: f.[γ] -->* f'
H2: irred f'
TApp f.[γ] e.[γ] -->* TApp f' e.[γ]
Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f': term
H1: f.[γ] -->* f'
H2: irred f'
H: TApp f.[γ] e.[γ] -->* TApp f' e.[γ]
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧ {Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f': term
H1: f.[γ] -->* f'
H2: irred f'
TApp f.[γ] e.[γ] -->* TApp f' e.[γ] apply app_cong1; auto. }Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ → f.[γ] ∈ 𝓔⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f': term
H1: f.[γ] -->* f'
H2: irred f'
H: TApp f.[γ] e.[γ] -->* TApp f' e.[γ]
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    unfold sem_expr in IHHe1.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    f.[γ] -->* e'
    → irred e' → e' ∈ 𝓥⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f': term
H1: f.[γ] -->* f'
H2: irred f'
H: TApp f.[γ] e.[γ] -->* TApp f' e.[γ]
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧ specialize IHHe1 with f'.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
f': term
IHHe1: valid_subst Γ γ
→ f.[γ] -->* f' → irred f' → f' ∈ 𝓥⟦ τ₂ ⇒ τ ⟧
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
H1: f.[γ] -->* f'
H2: irred f'
H: TApp f.[γ] e.[γ] -->* TApp f' e.[γ]
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    rewrite sem_value_arr in IHHe1.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
f': term
IHHe1: valid_subst Γ γ
→ f.[γ] -->* f'
  → irred f'
    → ∃ e : {bind term},
        f' = TLam τ₂ e
        ∧ (∀ v : term,
             v ∈ 𝓥⟦ τ₂ ⟧ → e.[v/] ∈ 𝓔⟦ τ ⟧)
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
H1: f.[γ] -->* f'
H2: irred f'
H: TApp f.[γ] e.[γ] -->* TApp f' e.[γ]
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    destruct IHHe1 as [f'' [Hf' Hf'']]; auto.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
f': term
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
H1: f.[γ] -->* f'
H2: irred f'
H: TApp f.[γ] e.[γ] -->* TApp f' e.[γ]
f'': {bind term}
Hf': f' = TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    subst.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    assert (TApp (TLam τ₂ f'') e.[γ] -->* e').Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
TApp (TLam τ₂ f'') e.[γ] -->* e'
Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    {Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
TApp (TLam τ₂ f'') e.[γ] -->* e' eapply irred_unique; [apply Hstep | |]; auto. }Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    destruct (app_lemma2 He' H0) as [e2' [? ?]].Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe2: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
e2': term
H3: e.[γ] -->* e2'
H4: irred e2'
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    unfold sem_expr in IHHe2.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
IHHe2: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e' → irred e' → e' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
e2': term
H3: e.[γ] -->* e2'
H4: irred e2'
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    specialize IHHe2 with e2'.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
∃ e'' : term, (e'' -->* e') ∧ e'' ∈ 𝓔⟦ τ ⟧
    exists (f''.[e2'/]); split.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
f''.[e2'/] -->* e'
Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
f''.[e2'/] ∈ 𝓔⟦ τ ⟧
    +Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
f''.[e2'/] -->* e' eapply irred_unique; eauto.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
TApp (TLam τ₂ f'') e.[γ] -->* f''.[e2'/]
      apply multistep_trans with (TApp (TLam τ₂ f'') e2').Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
TApp (TLam τ₂ f'') e.[γ] -->* TApp (TLam τ₂ f'') e2'
Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
TApp (TLam τ₂ f'') e2' -->* f''.[e2'/]
      apply app_cong2; auto.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
TApp (TLam τ₂ f'') e2' -->* f''.[e2'/]
      econstructor; auto.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
TApp (TLam τ₂ f'') e2' --> f''.[e2'/] constructor; [eapply sem_value_is_value; eauto | reflexivity].
    +Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
f''.[e2'/] ∈ 𝓔⟦ τ ⟧ apply Hf''.Γ: context
f, e: term
τ, τ₂: type
He1: Γ ⊢ f ∈ τ₂ ⇒ τ
He2: Γ ⊢ e ∈ τ₂
γ: var → term
e2': term
IHHe2: valid_subst Γ γ
→ e.[γ] -->* e2' → irred e2' → e2' ∈ 𝓥⟦ τ₂ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TApp f.[γ] e.[γ] -->* e'
He': irred e'
f'': {bind term}
H: TApp f.[γ] e.[γ] -->* TApp (TLam τ₂ f'') e.[γ]
H2: irred (TLam τ₂ f'')
H1: f.[γ] -->* TLam τ₂ f''
Hf'': ∀ v : term, v ∈ 𝓥⟦ τ₂ ⟧ → f''.[v/] ∈ 𝓔⟦ τ ⟧
H0: TApp (TLam τ₂ f'') e.[γ] -->* e'
H3: e.[γ] -->* e2'
H4: irred e2'
e2' ∈ 𝓥⟦ τ₂ ⟧ apply IHHe2; auto.

  - (* If case *)Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
IHHe1: Γ ⊧ e ∈ Bool
IHHe2: Γ ⊧ e₁ ∈ τ
IHHe3: Γ ⊧ e₂ ∈ τ
γ: var → term
Hγ: valid_subst Γ γ
TIf e.[γ] e₁.[γ] e₂.[γ] ∈ 𝓔⟦ τ ⟧ unfold sem_has_type in IHHe1, IHHe2, IHHe3.Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
IHHe1: ∀ γ : var → term,
  valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ Bool ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
γ: var → term
Hγ: valid_subst Γ γ
TIf e.[γ] e₁.[γ] e₂.[γ] ∈ 𝓔⟦ τ ⟧
    specialize IHHe1 with γ.Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ Bool ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
TIf e.[γ] e₁.[γ] e₂.[γ] ∈ 𝓔⟦ τ ⟧
    intros e' Hstep He'.Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ → e.[γ] ∈ 𝓔⟦ Bool ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
e' ∈ 𝓥⟦ τ ⟧
    unfold sem_expr in IHHe1.Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e' → irred e' → e' ∈ 𝓥⟦ Bool ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
e' ∈ 𝓥⟦ τ ⟧
    destruct (tif_lemma _ _ _ He' _ Hstep) as [e1' [Hif1 Hif2]].Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e' → irred e' → e' ∈ 𝓥⟦ Bool ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
e1': term
Hif1: e.[γ] -->* e1'
Hif2: irred e1'
e' ∈ 𝓥⟦ τ ⟧
    assert (TIf e.[γ] e₁.[γ] e₂.[γ] -->* TIf e1' e₁.[γ] e₂.[γ]).Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e' → irred e' → e' ∈ 𝓥⟦ Bool ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
e1': term
Hif1: e.[γ] -->* e1'
Hif2: irred e1'
TIf e.[γ] e₁.[γ] e₂.[γ] -->* TIf e1' e₁.[γ] e₂.[γ]
Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e' → irred e' → e' ∈ 𝓥⟦ Bool ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
e1': term
Hif1: e.[γ] -->* e1'
Hif2: irred e1'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->* TIf e1' e₁.[γ] e₂.[γ]
e' ∈ 𝓥⟦ τ ⟧
    {Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e' → irred e' → e' ∈ 𝓥⟦ Bool ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
e1': term
Hif1: e.[γ] -->* e1'
Hif2: irred e1'
TIf e.[γ] e₁.[γ] e₂.[γ] -->* TIf e1' e₁.[γ] e₂.[γ] auto using if_cond_cong. }Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e' → irred e' → e' ∈ 𝓥⟦ Bool ⟧
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
e1': term
Hif1: e.[γ] -->* e1'
Hif2: irred e1'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->* TIf e1' e₁.[γ] e₂.[γ]
e' ∈ 𝓥⟦ τ ⟧
    simpl in IHHe1.Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
e1': term
Hif1: e.[γ] -->* e1'
Hif2: irred e1'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->* TIf e1' e₁.[γ] e₂.[γ]
e' ∈ 𝓥⟦ τ ⟧
    destruct (IHHe1 Hγ e1') as [? | ?]; auto; subst.Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TTrue e₁.[γ] e₂.[γ]
Hif2: irred TTrue
Hif1: e.[γ] -->* TTrue
e' ∈ 𝓥⟦ τ ⟧
Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TFalse e₁.[γ] e₂.[γ]
Hif2: irred TFalse
Hif1: e.[γ] -->* TFalse
e' ∈ 𝓥⟦ τ ⟧
    *Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TTrue e₁.[γ] e₂.[γ]
Hif2: irred TTrue
Hif1: e.[γ] -->* TTrue
e' ∈ 𝓥⟦ τ ⟧ assert (e₁.[γ] -->* e').Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TTrue e₁.[γ] e₂.[γ]
Hif2: irred TTrue
Hif1: e.[γ] -->* TTrue
e₁.[γ] -->* e'
Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TTrue e₁.[γ] e₂.[γ]
Hif2: irred TTrue
Hif1: e.[γ] -->* TTrue
H0: e₁.[γ] -->* e'
e' ∈ 𝓥⟦ τ ⟧
      {Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TTrue e₁.[γ] e₂.[γ]
Hif2: irred TTrue
Hif1: e.[γ] -->* TTrue
e₁.[γ] -->* e' eapply irred_unique; [| | auto].Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TTrue e₁.[γ] e₂.[γ]
Hif2: irred TTrue
Hif1: e.[γ] -->* TTrue
?a -->* e'
Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TTrue e₁.[γ] e₂.[γ]
Hif2: irred TTrue
Hif1: e.[γ] -->* TTrue
?a -->* e₁.[γ]
        apply Hstep.Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TTrue e₁.[γ] e₂.[γ]
Hif2: irred TTrue
Hif1: e.[γ] -->* TTrue
TIf e.[γ] e₁.[γ] e₂.[γ] -->* e₁.[γ]
        apply multistep_trans with (TIf TTrue e₁.[γ] e₂.[γ]); auto. }Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TTrue e₁.[γ] e₂.[γ]
Hif2: irred TTrue
Hif1: e.[γ] -->* TTrue
H0: e₁.[γ] -->* e'
e' ∈ 𝓥⟦ τ ⟧
      eapply IHHe2; eauto.
    *Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TFalse e₁.[γ] e₂.[γ]
Hif2: irred TFalse
Hif1: e.[γ] -->* TFalse
e' ∈ 𝓥⟦ τ ⟧ assert (e₂.[γ] -->* e').Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TFalse e₁.[γ] e₂.[γ]
Hif2: irred TFalse
Hif1: e.[γ] -->* TFalse
e₂.[γ] -->* e'
Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TFalse e₁.[γ] e₂.[γ]
Hif2: irred TFalse
Hif1: e.[γ] -->* TFalse
H0: e₂.[γ] -->* e'
e' ∈ 𝓥⟦ τ ⟧
      {Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TFalse e₁.[γ] e₂.[γ]
Hif2: irred TFalse
Hif1: e.[γ] -->* TFalse
e₂.[γ] -->* e' eapply irred_unique; [| | auto].Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TFalse e₁.[γ] e₂.[γ]
Hif2: irred TFalse
Hif1: e.[γ] -->* TFalse
?a -->* e'
Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TFalse e₁.[γ] e₂.[γ]
Hif2: irred TFalse
Hif1: e.[γ] -->* TFalse
?a -->* e₂.[γ]
        apply Hstep.Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TFalse e₁.[γ] e₂.[γ]
Hif2: irred TFalse
Hif1: e.[γ] -->* TFalse
TIf e.[γ] e₁.[γ] e₂.[γ] -->* e₂.[γ]
        apply multistep_trans with (TIf TFalse e₁.[γ] e₂.[γ]); auto. }Γ: context
e, e₁, e₂: term
τ: type
He1: Γ ⊢ e ∈ Bool
He2: Γ ⊢ e₁ ∈ τ
He3: Γ ⊢ e₂ ∈ τ
γ: var → term
IHHe1: valid_subst Γ γ
→ ∀ e' : term,
    e.[γ] -->* e'
    → irred e' → e' = TTrue ∨ e' = TFalse
IHHe2: ∀ γ : var → term,
  valid_subst Γ γ → e₁.[γ] ∈ 𝓔⟦ τ ⟧
IHHe3: ∀ γ : var → term,
  valid_subst Γ γ → e₂.[γ] ∈ 𝓔⟦ τ ⟧
Hγ: valid_subst Γ γ
e': term
Hstep: TIf e.[γ] e₁.[γ] e₂.[γ] -->* e'
He': irred e'
H: TIf e.[γ] e₁.[γ] e₂.[γ] -->*
TIf TFalse e₁.[γ] e₂.[γ]
Hif2: irred TFalse
Hif1: e.[γ] -->* TFalse
H0: e₂.[γ] -->* e'
e' ∈ 𝓥⟦ τ ⟧
      eapply IHHe3; eauto.
Qed.

As promised, type safety follows as an easy corollary.

Corollary type_safety : ∀ τ t, ⊢ t ∈ τ → safe t.∀ (τ : type) (t : term), ⊢ t ∈ τ → safe t
Proof.∀ (τ : type) (t : term), ⊢ t ∈ τ → safe t
  eauto using fund_lemma, sem_type_implies_safe.
Qed.
End TypeSafety.

References

This note is based off Amal Ahmed's lectures on logical relations.