]> matita.cs.unibo.it Git - helm.git/commit
Proof of unicity of proofs for:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 2 Nov 2005 18:43:09 +0000 (18:43 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 2 Nov 2005 18:43:09 +0000 (18:43 +0000)
commit69dc6031c9e0574fa7a74ced74deeb7f9ec5695b
treeff3416e30822e827fc98ec01e9705e35a16d8027
parent7f842db771e5c3a4e9dbefb56dd1005b229ed214
Proof of unicity of proofs for:
 1. decidable equalities
 2. P x = true for some function P
helm/matita/library/datatypes/bool.ma
helm/matita/library/logic/connectives.ma
helm/matita/library/logic/equality.ma