proposition: Theorem norm_f : forall t ty, TyRel [] t ty -> norm [::] t.
proof: Proof. intros. pose (val := fun _ : name => norm_pred). assert (interp_term ty val [::] t). - apply ty_safe with (ctx := []); auto. + intro; simpl; apply computable_norm. + intro n; destruct n; simpl; intros; congruence. - assert (comp : computable (interp_pair ty val)) by (unfold interp_pair; apply computable_interp_term; intro; simpl; apply computable_norm). destruct comp; auto. Qed.
imports: List Arith Bool