diff --git a/theories/type_systems/stlc/auto_step.v b/theories/type_systems/stlc/auto_step.v
new file mode 100644
index 0000000..2019bdd
--- /dev/null
+++ b/theories/type_systems/stlc/auto_step.v
@@ -0,0 +1,177 @@
+From stdpp Require Import base relations tactics.
+From iris Require Import prelude.
+From semantics.lib Require Import sets maps.
+From semantics.ts.stlc Require Import lang notation.
+
+Fixpoint eval_step (e: expr): option expr :=
+  match e with
+    | Var _ => None
+    | Lam x body => None
+    | LitInt n => None
+    | App lhs rhs => match to_val rhs, to_val lhs with
+      | None, _ => fmap (λ (rhs': expr), App lhs rhs') (eval_step rhs)
+      | Some _, None => fmap (λ (lhs': expr), App lhs' rhs) (eval_step lhs)
+      | Some rhs', Some (LamV name body) => Some (subst' name rhs' body)
+      | _, _ => None
+      end
+    | Plus lhs rhs => match to_val rhs, to_val lhs with
+      | None, _ => fmap (λ (rhs': expr), Plus lhs rhs') (eval_step rhs)
+      | Some _, None => fmap (λ (lhs': expr), Plus lhs' rhs) (eval_step lhs)
+      | Some (LitIntV rhs'), Some (LitIntV lhs') => Some (LitInt (lhs' + rhs'))
+      | _, _ => None
+      end
+  end.
+
+Theorem step_eval_step (e e': expr): step e e' → eval_step e = Some e'.
+Proof.
+  intro H_step.
+  induction H_step; unfold eval_step; fold eval_step.
+  - unfold to_val.
+    destruct e'; try (unfold is_val in H; exfalso; exact H).
+    reflexivity.
+    reflexivity.
+  - destruct e1; try (unfold eval_step in IHH_step; discriminate IHH_step).
+    + unfold to_val.
+      destruct e2; try (unfold is_val in H; exfalso; exact H).
+      all: rewrite IHH_step; reflexivity.
+    + unfold to_val.
+      destruct e2; try (unfold is_val in H; exfalso; exact H).
+      all: rewrite IHH_step; reflexivity.
+  - destruct (to_val e2) eqn:H_to_val.
+    {
+      apply of_to_val in H_to_val.
+      assert (is_val (of_val v)); try exact (is_val_of_val v).
+      apply val_no_step in H_step.
+      exfalso; exact H_step.
+      rewrite <-H_to_val.
+      assumption.
+    }
+    rewrite IHH_step.
+    reflexivity.
+  - unfold to_val.
+    rewrite H.
+    reflexivity.
+  - destruct e2; try (unfold is_val in H; exfalso; exact H).
+    unfold to_val.
+
+    destruct H_step; try (rewrite IHH_step; reflexivity).
+    unfold to_val.
+    rewrite IHH_step; simpl.
+    destruct e1.
+    + inversion H_step.
+    + val_no_step.
+    + reflexivity.
+    + val_no_step.
+    + reflexivity.
+  - destruct (to_val e2) eqn:H_to_val.
+    {
+      apply of_to_val in H_to_val.
+      assert (is_val (of_val v)); try exact (is_val_of_val v).
+      apply val_no_step in H_step.
+      exfalso; exact H_step.
+      rewrite <-H_to_val.
+      assumption.
+    }
+    rewrite IHH_step.
+    reflexivity.
+Qed.
+
+Theorem eval_step_step (e e': expr): eval_step e = Some e' → step e e'.
+Proof.
+  revert e'.
+  induction e; intros e' H_eq.
+  all: try (unfold eval_step in H_eq; discriminate H_eq).
+  - unfold eval_step in H_eq; fold eval_step in H_eq.
+
+    induction (eval_step e2).
+    + remember (IHe2 a (eq_refl _)) as H_appr.
+      unfold eval_step in H_eq; fold eval_step in H_eq.
+      destruct (to_val e2) eqn:H_to_val.
+      clear HeqH_appr.
+      {
+        apply of_to_val in H_to_val.
+        assert (is_val (of_val v)); try exact (is_val_of_val v).
+        apply val_no_step in H_appr.
+        exfalso; exact H_appr.
+        rewrite <-H_to_val.
+        assumption.
+      }
+      simpl in H_eq.
+      injection H_eq; intro H_eq'.
+      rewrite <-H_eq'.
+      apply StepAppR.
+      assumption.
+    + destruct (to_val e2) eqn:H_e2_to_val.
+      all: destruct (to_val e1) eqn:H_e1_to_val.
+      all: try (simpl in H_eq; discriminate H_eq).
+      all: try remember (of_to_val _ _ H_e1_to_val) as H_e1_val.
+      all: try remember (of_to_val _ _ H_e2_to_val) as H_e2_val.
+      {
+        subst.
+        induction v0.
+        discriminate H_eq.
+        injection H_eq; intro H_eq'; subst.
+        apply StepBeta.
+        eauto.
+      }
+      induction (eval_step e1).
+      {
+        simpl in H_eq.
+        injection H_eq; intro H_eq'.
+        rewrite <-H_eq'.
+        eapply StepAppL.
+        rewrite <-H_e2_val.
+        apply is_val_of_val.
+        apply (IHe1 a (eq_refl _)).
+      }
+      simpl in H_eq; discriminate H_eq.
+  - unfold eval_step in H_eq; fold eval_step in H_eq.
+    destruct (to_val e2) eqn:H_e2_to_val.
+    all: destruct (to_val e1) eqn:H_e1_to_val.
+    all: try remember (of_to_val _ _ H_e1_to_val) as H_e1_val.
+    all: try remember (of_to_val _ _ H_e2_to_val) as H_e2_val.
+    + induction v; induction v0; try discriminate H_eq.
+      rewrite <-H_e2_val.
+      rewrite <-H_e1_val.
+      unfold of_val.
+      injection H_eq; intro H_eq'.
+      rewrite <-H_eq'.
+      eauto.
+    + induction v; try discriminate H_eq.
+      all: (
+        unfold of_val in H_e2_val;
+        rewrite <-H_e2_val;
+        induction (eval_step e1); try (simpl in H_eq; discriminate H_eq);
+        simpl in H_eq;
+        injection H_eq; intro H_eq';
+        subst;
+        eapply StepPlusL;
+        unfold is_val; intuition;
+        exact (IHe1 a (eq_refl _))
+      ).
+    + induction (eval_step e2); try (simpl in H_eq; discriminate H_eq).
+      simpl in H_eq; injection H_eq; intro H_eq'.
+      subst.
+      eapply StepPlusR.
+      exact (IHe2 a (eq_refl _)).
+    + induction (eval_step e2); try (simpl in H_eq; discriminate H_eq).
+      simpl in H_eq; injection H_eq; intro H_eq'.
+      subst.
+      eapply StepPlusR.
+      exact (IHe2 a (eq_refl _)).
+Qed.
+
+
+Ltac auto_subst :=
+  (rewrite subst_closed_nil; last assumption) ||
+  (unfold subst'; unfold subst; simpl; fold subst).
+
+Ltac auto_step := (simpl;
+  repeat (eapply rtc_l;
+    first apply eval_step_step;
+    first simpl;
+    first reflexivity;
+    try (reflexivity; done)
+  );
+  reflexivity
+).
diff --git a/theories/type_systems/stlc/exercises02_sol.v b/theories/type_systems/stlc/exercises02_sol.v
index 59d035c..e50cc3e 100644
--- a/theories/type_systems/stlc/exercises02_sol.v
+++ b/theories/type_systems/stlc/exercises02_sol.v
@@ -375,4 +375,4 @@ Section prove_non_existence.
   Proof.
     (* This is not possible as shown above *)
   Abort.
-End prove_non_existence.
\ No newline at end of file
+End prove_non_existence.
diff --git a/theories/type_systems/stlc/lang.v b/theories/type_systems/stlc/lang.v
index caafae6..a463e2f 100644
--- a/theories/type_systems/stlc/lang.v
+++ b/theories/type_systems/stlc/lang.v
@@ -336,4 +336,4 @@ Ltac val_no_step :=
   match goal with
   | [H: step ?e1 ?e2 |- _] =>
     solve [exfalso; eapply (val_no_step _ _ H); done]
-  end.
\ No newline at end of file
+  end.
diff --git a/theories/type_systems/stlc_extended/bigstep.v b/theories/type_systems/stlc_extended/bigstep.v
index 372f3d4..61c940d 100644
--- a/theories/type_systems/stlc_extended/bigstep.v
+++ b/theories/type_systems/stlc_extended/bigstep.v
@@ -10,21 +10,45 @@ Implicit Types
 
 Inductive big_step : expr → val → Prop :=
   | bs_lit (n : Z) :
-      big_step (LitInt n) (LitIntV n)
+    big_step (LitInt n) (LitIntV n)
   | bs_lam (x : binder) (e : expr) :
-      big_step (λ: x, e)%E (λ: x, e)%V
+    big_step (λ: x, e)%E (λ: x, e)%V
   | bs_add e1 e2 (z1 z2 : Z) :
-      big_step e1 (LitIntV z1) →
-      big_step e2 (LitIntV z2) →
-      big_step (Plus e1 e2) (LitIntV (z1 + z2))%Z
+    big_step e1 (LitIntV z1) →
+    big_step e2 (LitIntV z2) →
+    big_step (Plus e1 e2) (LitIntV (z1 + z2))%Z
   | bs_app e1 e2 x e v2 v :
-      big_step e1 (LamV x e) →
-      big_step e2 v2 →
-      big_step (subst' x (of_val v2) e) v →
-      big_step (App e1 e2) v
-
-(* TODO : extend the big-step semantics *)
-    .
+    big_step e1 (LamV x e) →
+    big_step e2 v2 →
+    big_step (subst' x (of_val v2) e) v →
+    big_step (App e1 e2) v
+  (* Pairs and fst, snd *)
+  | bs_pair (e1 e2 : expr) (v1 v2 : val) :
+    big_step e1 v1 →
+    big_step e2 v2 →
+    big_step (Pair e1 e2) (PairV v1 v2)
+  | bs_fst (e : expr) (v1 v2: val):
+    big_step e (PairV v1 v2) →
+    big_step (Fst e) v1
+  | bs_snd (e : expr) (v1 v2: val):
+    big_step e (PairV v1 v2) →
+    big_step (Fst e) v1
+  (* Inj *)
+  | bs_inj_l e v :
+    big_step e v →
+    big_step (InjL e) (InjLV v)
+  | bs_inj_r e v :
+    big_step e v →
+    big_step (InjR e) (InjRV v)
+  | bs_case_l (e_inj e_l e_r: expr) (v_inj v: val):
+    big_step e_inj (InjLV v_inj) →
+    big_step (e_l (of_val v_inj)) v →
+    big_step (Case e_inj e_l e_r) v
+  | bs_case_r (e_inj e_l e_r: expr) (v_inj v: val):
+    big_step e_inj (InjRV v_inj) →
+    big_step (e_r (of_val v_inj)) v →
+    big_step (Case e_inj e_l e_r) v
+.
 #[export] Hint Constructors big_step : core.
 
 Lemma big_step_of_val e v :
@@ -33,9 +57,7 @@ Lemma big_step_of_val e v :
 Proof.
   intros ->.
   induction v; simpl; eauto.
-
-(* TODO : this should be fixed once you have added the right semantics *)
-Admitted.
+Qed.
 
 
 Lemma big_step_val v v' :
diff --git a/theories/type_systems/stlc_extended/ctxstep.v b/theories/type_systems/stlc_extended/ctxstep.v
index f2bef44..d3761d9 100644
--- a/theories/type_systems/stlc_extended/ctxstep.v
+++ b/theories/type_systems/stlc_extended/ctxstep.v
@@ -12,7 +12,24 @@ Inductive base_step : expr → expr → Prop :=
      e2 = (LitInt n2) →
      (n1 + n2)%Z = n3 →
      base_step (Plus e1 e2) (LitInt n3)
-  (* TODO: extend the definition *)
+  | FstS e v1 v2:
+    is_val v1 →
+    is_val v2 →
+    e = (Pair v1 v2) →
+    base_step (Fst e) v1
+  | SndS e v1 v2:
+    is_val v1 →
+    is_val v2 →
+    e = (Pair v1 v2) →
+    base_step (Snd e) v2
+  | CaseLS v_inj v e1 e2:
+    is_val v_inj →
+    v_inj = (InjL v) →
+    base_step (Case v_inj e1 e2) (App e1 v)
+  | CaseRS v_inj v e1 e2:
+    is_val v_inj →
+    v_inj = (InjR v) →
+    base_step (Case v_inj e1 e2) (App e2 v)
 .
 
 #[export] Hint Constructors base_step : core.
@@ -24,7 +41,13 @@ Inductive ectx :=
   | AppRCtx (e1 : expr) (K: ectx)
   | PlusLCtx (K: ectx) (v2 : val)
   | PlusRCtx (e1 : expr) (K: ectx)
-  (* TODO: extend the definition *)
+  | PairLCtx (K: ectx) (v2: val)
+  | PairRCtx (e1: expr) (K: ectx)
+  | FstCtx (K: ectx)
+  | SndCtx (K: ectx)
+  | InjLCtx (K: ectx)
+  | InjRCtx (K: ectx)
+  | CaseCtx (K: ectx) (e1: expr) (e2: expr)
 .
 
 Fixpoint fill (K : ectx) (e : expr) : expr :=
@@ -34,7 +57,13 @@ Fixpoint fill (K : ectx) (e : expr) : expr :=
   | AppRCtx e1 K => App e1 (fill K e)
   | PlusLCtx K v2 => Plus (fill K e) (of_val v2)
   | PlusRCtx e1 K => Plus e1 (fill K e)
-  (* TODO: extend the definition *)
+  | PairLCtx K v2 => Pair (fill K e) (of_val v2)
+  | PairRCtx e1 K => Pair e1 (fill K e)
+  | FstCtx K => Fst (fill K e)
+  | SndCtx K => Snd (fill K e)
+  | InjLCtx K => InjL (fill K e)
+  | InjRCtx K => InjR (fill K e)
+  | CaseCtx K e1 e2 => Case (fill K e) e1 e2
   end.
 
 Fixpoint comp_ectx (K: ectx) (K' : ectx) : ectx :=
@@ -44,7 +73,13 @@ Fixpoint comp_ectx (K: ectx) (K' : ectx) : ectx :=
   | AppRCtx e1 K => AppRCtx e1 (comp_ectx K K')
   | PlusLCtx K v2 => PlusLCtx (comp_ectx K K') v2
   | PlusRCtx e1 K => PlusRCtx e1 (comp_ectx K K')
-  (* TODO: extend the definition *)
+  | PairLCtx K v2 => PairLCtx (comp_ectx K K') v2
+  | PairRCtx e1 K => PairRCtx e1 (comp_ectx K K')
+  | FstCtx K => FstCtx (comp_ectx K K')
+  | SndCtx K => SndCtx (comp_ectx K K')
+  | InjLCtx K => InjLCtx (comp_ectx K K')
+  | InjRCtx K => InjRCtx (comp_ectx K K')
+  | CaseCtx K e1 e2 => CaseCtx (comp_ectx K K') e1 e2
   end.
 
 (** Contextual steps *)
@@ -116,61 +151,79 @@ Proof.
   by eapply (fill_contextual_step (PlusRCtx e1 HoleCtx)).
 Qed.
 
+Ltac is_val_to_val v H :=
+  rewrite (is_val_spec _) in H; destruct H as [v H]; apply of_to_val in H; symmetry in H.
+
 Lemma contextual_step_pair_l e1 e1' e2:
   is_val e2 →
   contextual_step e1 e1' →
   contextual_step (Pair e1 e2) (Pair e1' e2).
 Proof.
-  (* TODO: exercise *)
-Admitted.
-
+  intros H_val H_ctx.
+  is_val_to_val v2 H_val.
+  rewrite H_val.
+  eapply (fill_contextual_step (PairLCtx HoleCtx v2)).
+  assumption.
+Qed.
 
 Lemma contextual_step_pair_r e1 e2 e2':
   contextual_step e2 e2' →
   contextual_step (Pair e1 e2) (Pair e1 e2').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (PairRCtx e1 HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_fst e e':
   contextual_step e e' →
   contextual_step (Fst e) (Fst e').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (FstCtx HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_snd e e':
   contextual_step e e' →
   contextual_step (Snd e) (Snd e').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (SndCtx HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_injl e e':
   contextual_step e e' →
   contextual_step (InjL e) (InjL e').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (InjLCtx HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_injr e e':
   contextual_step e e' →
   contextual_step (InjR e) (InjR e').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (InjRCtx HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_case e e' e1 e2:
   contextual_step e e' →
   contextual_step (Case e e1 e2) (Case e' e1 e2).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (CaseCtx HoleCtx e1 e2)).
+  assumption.
+Qed.
 
 
 #[global]