Axiomatic proofs of natural addition properties, in Idris
Inlining the second clause fails because you're shadowing Refl.

plus_assoc (S a) b c = let Refl = plus_assoc a b c in Refl

just reduces to

plus_assoc (S a) b c = plus_assoc a b c