Inductive term : Set :=
  | sqop : term
  | squiggle : term -> term
  | squaggle : term -> term
  | transmogrify : term -> term -> term.

Inductive value: term -> Prop :=
| value_sqop :
    value sqop
| value_squiggle : forall t : term,
    value t ->
    value (squiggle t).

Inductive step : term -> term -> Prop :=
| step_squiggle : forall t t' : term,
    step t t' ->
    step (squiggle t) (squiggle t')
| step_squaggle : forall t : term,
    step (squaggle t) t.

Inductive type : Set := W.

Inductive typing : term -> type -> Prop :=
| typing_sqop :
    typing sqop W
| typing_squiggle : forall t : term,
    typing t W ->
    typing (squiggle t) W
| typing_squaggle : forall t : term, forall T : type,
    typing t T ->
    typing (squaggle t) T.

Section Exercise1.

Definition type1 : typing (squiggle sqop) W :=
  typing_squiggle sqop (typing_sqop).

Definition type2 : typing (squaggle (squiggle (squaggle sqop))) W :=
  typing_squaggle (squiggle (squaggle sqop)) W (
    typing_squiggle (squaggle sqop) (
      typing_squaggle sqop W (
        typing_sqop))).

End Exercise1.


Section Exercise2.

Definition step2 : step (squaggle (squiggle (squaggle sqop))) (squiggle (squaggle sqop)) :=
  step_squaggle (squiggle (squaggle (sqop))).
  
End Exercise2.

Section Exercise3.

Lemma progress : forall t : term, forall T : type, typing t T -> value t \/ (exists t' : term, step t t').
  intros t T TH.
  induction TH.

  left.
  exact value_sqop.

  induction IHTH.

    left.
    apply value_squiggle.
    assumption.

    right.
    destruct H.
    exists (squiggle x).
    apply step_squiggle.
    assumption.

  right.
  exists t.
  apply step_squaggle.

  Qed.

Lemma preservation : forall t t' : term, forall T : type, typing t T -> step t t' -> typing t' T.
  intros t t' T TH SH.
    generalize dependent t'.
    induction TH.

      intros t' SH.
      inversion SH.

      intros t' SH.
      inversion SH.
      apply typing_squiggle.
      apply IHTH.
      assumption.
      
      intros t' SH.
      inversion SH.
      subst t'.
      assumption.

    Qed.

End Exercise3.