proposition: Lemma freevars_in_allvars : ( (forall (gs : GSym G) (t : Term gs), subset (tfreevars vc t) (tAllVars t)) * (forall (gs : GSym G) (p : Pattern gs), subset (pfreevars vc p) (pAllVars p)) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) lbvars, subset (mfreevars vc m lbvars) (mAllVars m)) ).
proof: Proof. GInduction; auto; introv; try (complete (allsimpl; cpx)); try (complete (allsimpl; introv f e; DDeqs; cpx; rw subtractv_nil_l; auto)). - Case "mtcons". allsimpl. introv ss M; introv. destruct lbvars; allsimpl; apply subset_app_lr; auto. unfold subtractv. apply subset_diff. apply subset_app_r; auto. - Case "mpcons". allsimpl. introv ss M; introv. destruct lbvars; allsimpl; apply subset_app_lr; auto. unfold subtractv. apply subset_diff. apply subset_app_r; auto. Qed.
imports: AlphaEquality SwapProps Eqdep_dec