diff options
| author |  Rutger Broekhoff | 2024-06-27 02:13:26 +0200 |
|---|---|---|
| committer | Rutger Broekhoff | 2024-06-27 02:13:26 +0200 |
| commit | 5aef9a66966c8aa97041461d618b601e60e56c91 (patch) | |
| tree | e437f49b12ad069731d61f6b95227de60d9ff88d /semprop.v | |
| parent | ba973b2fa09e0ff203eec9770908a88e0ccfde70 (diff) | |
| download | mininix-formalization-5aef9a66966c8aa97041461d618b601e60e56c91.tar.gz mininix-formalization-5aef9a66966c8aa97041461d618b601e60e56c91.zip | |
Be consistent in notation of simplify_eq/=
Diffstat (limited to 'semprop.v')
| -rw-r--r-- | semprop.v | 2 |
1 files changed, 1 insertions, 1 deletions
| @@ -42,7 +42,7 @@ Proof. | |||
| 42 | - exfalso. apply H. by exists bs. | 42 | - exfalso. apply H. by exists bs. |
| 43 | - f_equal. by eapply matches_deterministic. | 43 | - f_equal. by eapply matches_deterministic. |
| 44 | - apply map_insert_inv in H0 as [H01 H02]. | 44 | - apply map_insert_inv in H0 as [H01 H02]. |
| 45 | by simplify_eq /=. | 45 | by simplify_eq/=. |
| 46 | - f_equal. by eapply binop_deterministic. | 46 | - f_equal. by eapply binop_deterministic. |
| 47 | - rewrite H4 in H. by apply is_Some_None in H. | 47 | - rewrite H4 in H. by apply is_Some_None in H. |
| 48 | - exfalso. apply H4. by exists bs. | 48 | - exfalso. apply H4. by exists bs. |