proposition: Lemma subtractv_cons : forall {G : CFGV} {vc : VarSym G} a l1 l2, @subtractv G vc (a :: l1) l2 = if in_deq_t (vType vc) (DeqVtype vc) a l2 then subtractv l1 l2 else a :: (subtractv l1 l2).
proof: Proof. unfold subtractv, removev; simpl; introv. rw diff_cons_r. remember (memberb (DeqVtype vc) a l2); destruct b; symmetry in Heqb; [rw fold_assert in Heqb | rw not_of_assert in Heqb]; rw (@assert_memberb (vType vc)) in Heqb; destruct (in_deq_t (vType vc) (DeqVtype vc) a l2); sp. Qed.
imports: CFGV Omega Eqdep_dec