2010-01-26 Christian Urban added an LamEx example together with the new nominal infrastructure
2010-01-26 Cezary Kaliszyk Bex1_Bexeq_regular.
2010-01-26 Cezary Kaliszyk Hom Theorem with exists unique
2010-01-26 Cezary Kaliszyk 2 cases for regularize with split, lemmas with split now lift.
2010-01-26 Cezary Kaliszyk Simpler statement that has the problem.
2010-01-26 Cezary Kaliszyk Found a term that does not regularize.
Loading...
(0) -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 tip