IMPORTANT FIX

The final proof needs one more step. So instead of

Main.case_one_proof = proof { intro l; intro H; rewrite (sym H); trivial; }

You need this

Main.case_one_proof = proof { intro l; intro H; compute; rewrite (sym H); trivial; }

The extra “compute” is needed because Idris doesn’t (at present) simplify the goal before trying a rewrite step. (I’m used to proof assistants which do…)

Sorry about that!

You can see more discussion on this point at http://www.reddit.com/r/programming/comments/1bneoe/dependent_types_a_new_paradigm/c98aos8