dan/HITs-Examples
1
0
Fork 0
mirror of https://github.com/nmvdw/HITs-Examples synced 2025-11-03 23:23:51 +01:00
Code Issues Releases Wiki Activity

Cleaning in length

Browse Source
This commit is contained in:
Niels van der Weide
2017-09-26 13:06:47 +02:00
parent d7a95697fb
commit 72a44c71f9
1 changed files with 0 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
FiniteSets/kuratowski/length.v
View File

@@ -19,7 +19,6 @@ Section length.
destruct (m_dec_path a b) as [Hab | Hab]. destruct (m_dec_path a b) as [Hab | Hab].
+ strip_truncations. + strip_truncations.
rewrite Hab. rewrite Hab.
rewrite ?singleton_isIn_d_aa.
reflexivity. reflexivity.
+ rewrite ?singleton_isIn_d_false. + rewrite ?singleton_isIn_d_false.
++ simpl. ++ simpl.