(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
(* substitution ***************************************************************)
(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
(* substitution ***************************************************************)