Added coercion function with proof erasure using RULES pragma