Require Import base data.fintype f.types f.fcbvsyntax.

Inductive red {m} : tm m 0 -> vl m 0 -> Prop :=
| red_val v :
    red (val v) v
| red_app s t b u v :
    red s (lam b) ->
    red t u ->
    red (tm_inst (@tvar m) (u .: @var m 0) b) v ->
    red (app s t) v
| red_tapp s A b v :
    red s (tlam b) ->
    red (tm_inst (A .: @tvar m) (@var m 0) b) v ->
    red (tapp s A) v.