equal
deleted
inserted
replaced
292 (* FIXME /TODO needs to be adapted *) |
292 (* FIXME /TODO needs to be adapted *) |
293 (* |
293 (* |
294 To prove that the regularised theorem implies the abs/rep injected, |
294 To prove that the regularised theorem implies the abs/rep injected, |
295 we try: |
295 we try: |
296 |
296 |
297 1) theorems 'trans2' from the appropriate QUOT_TYPE |
297 1) theorems 'trans2' from the appropriate Quot_Type |
298 2) remove lambdas from both sides: lambda_rsp_tac |
298 2) remove lambdas from both sides: lambda_rsp_tac |
299 3) remove Ball/Bex from the right hand side |
299 3) remove Ball/Bex from the right hand side |
300 4) use user-supplied RSP theorems |
300 4) use user-supplied RSP theorems |
301 5) remove rep_abs from the right side |
301 5) remove rep_abs from the right side |
302 6) reflexivity of equality |
302 6) reflexivity of equality |