equal
deleted
inserted
replaced
403 case (Var a n) |
403 case (Var a n) |
404 then have "n < length (map ($ s) a)" by simp |
404 then have "n < length (map ($ s) a)" by simp |
405 then have "map ($ s) a |- Var n :: map ($ s) a ! n" |
405 then have "map ($ s) a |- Var n :: map ($ s) a ! n" |
406 by (rule has_type.Var) |
406 by (rule has_type.Var) |
407 also have "map ($ s) a ! n = $ s (a ! n)" |
407 also have "map ($ s) a ! n = $ s (a ! n)" |
408 by (rule nth_map) |
408 by (rule nth_map) (rule Var) |
409 also have "map ($ s) a = $ s a" |
409 also have "map ($ s) a = $ s a" |
410 by (simp only: app_subst_list) |
410 by (simp only: app_subst_list) |
411 finally show ?case . |
411 finally show ?case . |
412 next |
412 next |
413 case (Abs a e t1 t2) |
413 case (Abs a e t1 t2) |