fix minor wf_to_inners bug, change example3 to use termsem_cert