proposition: Lemma subtractv_app_r : forall {G : CFGV} {vc : VarSym G} (l1 l2 l : list (vType vc)), subtractv l (l1 ++ l2) = subtractv (subtractv l l2) l1.
proof: Proof. unfold subtractv; introv. rw diff_app_l; sp. Qed.
imports: CFGV Omega Eqdep_dec