]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3b3c065) | patch
The proof of append_cons used transitive_eq, not indexed.
authorAndrea Asperti <andrea.asperti@unibo.it>
Wed, 2 Nov 2011 10:58:34 +0000 (10:58 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Wed, 2 Nov 2011 10:58:34 +0000 (10:58 +0000)
commitcb4b0c887ba703b7949656d5b72b5f94756a77bd
tree8cb571c0b45fc0c480dc31b8e315b1af033fd374tree | snapshot
parent3b3c0659bdae6fe088604e00d1f0c0dc1b84202dcommit | diff
The proof of append_cons used transitive_eq, not indexed.
If other cases will present we shall reindex it.
matita/matita/lib/basics/list.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.