467 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   467 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   468 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   468 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   469 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   469 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   470 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   470 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   471 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   471 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})

   472 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})

   473 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})

   473 apply (rule IDENTITY_QUOTIENT)

   474 apply (rule IDENTITY_QUOTIENT)

   474 apply (rule FUN_QUOTIENT)

   475 apply (rule FUN_QUOTIENT)

   475 apply (rule QUOTIENT_fset)

   476 apply (rule QUOTIENT_fset)

   476 apply (rule IDENTITY_QUOTIENT)

   477 apply (rule IDENTITY_QUOTIENT)