@[derive decidable_eq]
inductive val : Type
| nat
| nil
| cons : Π (car : val) (cdr: val), val

@[derive decidable_eq]
inductive fn : val -> val -> Type
| zero : fn val.nil val.nat
| succ : fn val.nat val.nat
| car  : Π {tcar tcdr: val}, fn (val.cons tcar tcdr) tcar
| cdr  : Π {tcar tcdr: val}, fn (val.cons tcar tcdr) tcdr
| nil  : Π {tin : val}, fn tin val.nil
| cons : Π {tin tcar tcdr: val} (car : fn tin tcar) (cdr: fn tin tcdr), fn tin (val.cons tcar tcdr)
| comp : Π {tin tint tout: val} (f : fn tint tout) (g: fn tin tint), fn tin tout
| prec : Π {trest tout: val} (z_case : fn trest tout) (s_case: fn (val.cons val.nat (val.cons tout trest)) tout),
    fn (val.cons val.nat trest) tout

inductive step : Π {tin tout} (f: fn tin tout) (g: fn tin tout), Prop
| proj_car : Π {tin tcar tcdr} {car:fn tin tcar} {cdr: fn tin tcdr},
    step (fn.comp fn.car (fn.cons car cdr)) car
| proj_cdr : Π {tin tcar tcdr} {car:fn tin tcar} {cdr: fn tin tcdr},
    step (fn.comp fn.cdr (fn.cons car cdr)) cdr
| comp_f : Π {tin tint tout} {f1 f2:fn tint tout} {g: fn tin tint}
    (_ : step f1 f2),
    step (fn.comp f1 g) (fn.comp f2 g)

instance step_decidable :
    Π (tin tout) (f: fn tin tout) (g: fn tin tout),
    decidable (step f g) :=
begin
    intros,
    induction f,
    case comp {
        cases g,
        case comp {
            by_cases (f_tint = g_tint),
            focus {
                subst h,
                by_cases (f_g = g_g),
                focus {
                    subst h,
                    cases f_ih_f g_f,
                    case is_true {
                        apply (is_true),
                        constructor,
                        assumption,
                        done
                    },
                },
            },
            apply(is_false),
            intro h2,
            cases h2,
        },
    }
end