Awesome, thanks for the help :) I can find icombl <http://us.metamath.org/mpegif/icombl.html> and icombl1 <http://us.metamath.org/mpegif/icombl1.html>but can't find iocmbl and iocmbl1, am I right in thinking they don't exist? If so I could have a go at cooking them up.
Also I think maybe the proof of icombl1 could be shorted by using icombl. I haven't shortened a proof before, would this be helpful? Do I just edit the proof and then submit it? -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/39fc1f70-e15f-4fd6-8c86-d69f14f424c5%40googlegroups.com.
