equal
deleted
inserted
replaced
365 apply(clarsimp, blast dest!: boundedD) |
365 apply(clarsimp, blast dest!: boundedD) |
366 apply (erule pres_typeD) |
366 apply (erule pres_typeD) |
367 prefer 3 |
367 prefer 3 |
368 apply assumption |
368 apply assumption |
369 apply (erule listE_nth_in) |
369 apply (erule listE_nth_in) |
370 apply blast |
370 apply simp |
371 apply blast |
371 apply simp |
372 apply (subst decomp_propa) |
372 apply (subst decomp_propa) |
373 apply blast |
373 apply fast |
374 apply simp |
374 apply simp |
375 apply (rule conjI) |
375 apply (rule conjI) |
376 apply (rule merges_preserves_type) |
376 apply (rule merges_preserves_type) |
377 apply blast |
377 apply blast |
378 apply clarify |
378 apply clarify |
379 apply (rule conjI) |
379 apply (rule conjI) |
380 apply(clarsimp, blast dest!: boundedD) |
380 apply(clarsimp, fast dest!: boundedD) |
381 apply (erule pres_typeD) |
381 apply (erule pres_typeD) |
382 prefer 3 |
382 prefer 3 |
383 apply assumption |
383 apply assumption |
384 apply (erule listE_nth_in) |
384 apply (erule listE_nth_in) |
385 apply blast |
385 apply blast |