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