Inductive ty : Set :=
  | nat_ty : ty
  | bool_ty : ty
  | arr : ty -> ty -> ty.
Inductive vari : Set :=
    x : nat -> vari.

Inductive tm : Set :=
  | o : tm
  | ttt : tm
  | fff : tm
  | abs : vari -> ty -> tm -> tm
  | appl : tm -> tm -> tm
  | cond : tm -> tm -> tm -> tm
  | var : vari -> tm
  | succ : tm -> tm
  | prd : tm -> tm
  | is_o : tm -> tm
  | Fix : vari -> ty -> tm -> tm
  | clos : tm -> vari -> ty -> tm -> tm.