Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Add η principles for sigma types | 2017-03-01 | |
* | Added operation (including creating ) | 2017-02-27 | |
* | Modified lemma and created tactic to handle it; added reduce step to multipl... | 2017-02-26 | |
* | Merge new base system (#112) | 2017-02-22 | |
* | Add inversion_expr | 2017-02-01 | |
* | Make [inversion_{prod,sigma}] stronger | 2016-09-05 | |
* | Add documentation: Equality, HProp, Isomorphism, Sigma (#41) | 2016-08-01 | |
* | Remove useless hypotheses for [path_sigT_uncurried_iff] | 2016-08-01 | |
* | Add inversion helper tactics to Sigma.v | 2016-07-29 | |
* | Rename path_sig{,T}{ => _uncurried}_iff | 2016-07-29 | |
* | Add path_sig{,T}_iff | 2016-07-29 | |
* | Add some lemmas to Util.Sigma | 2016-07-29 | |
* | Set Asymmetric Patterns, add util lemmas about sig | 2016-07-29 |