Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 14:16:57 +0200] rev 124
Only QUOTIENSs are left to fnish proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:44:58 +0200] rev 123
More higher order unification problems
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:31:48 +0200] rev 122
Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:31:36 +0200] rev 121
Simplified
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:20:56 +0200] rev 120
Further in the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 11:54:50 +0200] rev 119
compose_tac works with the full instantiation.
Christian Urban <urbanc@in.tum.de> [Sat, 17 Oct 2009 12:19:06 +0200] rev 118
slightly simplified get_fun function
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 10:40:54 +0200] rev 117
The instantiated version is the same modulo beta
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 10:07:52 +0200] rev 116
Fully manually instantiated. Still fails...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 09:04:24 +0200] rev 115
Little progress with match/instantiate