fact: Definition norm_body (a : term) (norm : term -> term) := match a with | Srt s => Srt s | Ref n => Ref n | Abs T t => Abs (norm T) (norm t) | App u v => match norm u return term with | Abs _ b => norm (subst (norm v) b) | t => App t (norm v) end | Prod T U => Prod (norm T) (norm U) end.
imports: Peano_dec Transitive_Closure Union Termes Conv