make i2_Cv allow the exh to be extended

also, sketch out a proof of v_pat_syneq (still some serious cheats in
it). these two together allow me to prove two of the cheats in
compile_top_thm. i2_Cv maybe looks more dubious now though...