equal
deleted
inserted
replaced
369 apply (erule lift_IT) |
369 apply (erule lift_IT) |
370 apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] : IT") |
370 apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] : IT") |
371 apply (simp (no_asm_use)) |
371 apply (simp (no_asm_use)) |
372 apply (subgoal_tac "(Var 0 $$ map (\<lambda>t. lift t 0) |
372 apply (subgoal_tac "(Var 0 $$ map (\<lambda>t. lift t 0) |
373 (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] : IT") |
373 (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] : IT") |
374 apply (simp (no_asm_use) del: map_compose add: map_compose [symmetric] o_def) |
374 apply (simp (no_asm_use) del: map_compose |
|
375 add: map_compose [symmetric] o_def) |
375 apply (erule_tac x = "Ts =>> T" in allE) |
376 apply (erule_tac x = "Ts =>> T" in allE) |
376 apply (erule impE) |
377 apply (erule impE) |
377 apply simp |
378 apply simp |
378 apply (erule_tac x = "Var 0 $$ |
379 apply (erule_tac x = "Var 0 $$ |
379 map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) list)" in allE) |
380 map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) list)" in allE) |
443 apply (rule Var_IT) |
444 apply (rule Var_IT) |
444 apply (erule IT.Lambda) |
445 apply (erule IT.Lambda) |
445 apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT") |
446 apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT") |
446 apply simp |
447 apply simp |
447 apply (rule subst_type_IT) |
448 apply (rule subst_type_IT) |
448 apply (rule lists.Nil [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection] |
449 apply (rule lists.Nil |
449 foldl_Cons [THEN eq_reflection]]) |
450 [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection] |
|
451 foldl_Cons [THEN eq_reflection]]) |
450 apply (erule lift_IT) |
452 apply (erule lift_IT) |
451 apply (rule typing.App) |
453 apply (rule typing.App) |
452 apply (rule typing.Var) |
454 apply (rule typing.Var) |
453 apply simp |
455 apply simp |
454 apply (erule lift_type') |
456 apply (erule lift_type') |