proposition: Lemma freevars_swap_eq : ( (forall (gs : GSym G) (t : Term gs), forall (l1 l : list vcType), length l1 = length l -> disjoint l1 l -> tFresh l [t] -> tfreevars vc (tSwap t (combine l1 l)) = swapLVar (combine l1 l) (tfreevars vc t)) * (forall (gs : GSym G) (p : Pattern gs), forall (l1 l : list vcType), length l1 = length l -> disjoint l1 l -> pFresh l [p] -> pfreevars vc (pSwap p (combine l1 l)) = swapLVar (combine l1 l) (pfreevars vc p)) * (forall (lgs : list (bool * GSym G)) (m : Mixture lgs) lbvars, forall (l1 l : list vcType), length l1 = length l -> disjoint l1 l -> mFresh l [m] -> mfreevars vc (mSwap m (combine l1 l)) (swapLLVar (combine l1 l) lbvars) = swapLVar (combine l1 l) (mfreevars vc m lbvars)) ).
proof: Proof. GInduction; auto; introv; try (complete (allsimpl; cpx)); try (complete (allsimpl; introv f e; DDeqs; cpx; rw subtractv_nil_l; auto)). - Case "tnode". allsimpl. introv M len disj f. unfold allBndngVars. rewrite lBoundVars_swap. rw M; auto. - Case "pnode". allsimpl. introv M len disj f. apply (M []); auto. - Case "mtcons". allsimpl. introv T M len disj f. destruct lbvars; simpl; rewrite swapLVar_app; apply app_if. + apply T; auto; try (complete (unfold mFresh in f; unfold mFresh, tFresh; allsimpl; allrw disjoint_app_r; sp)). + apply (M []); auto; try (complete (unfold mFresh in f; unfold mFresh; allsimpl; allrw disjoint_app_r; sp)). + rewrite swapLVar_subtractv. rw T; auto; try (complete (unfold mFresh in f; unfold mFresh, tFresh; allsimpl; allrw disjoint_app_r; sp)). + apply M; auto; try (complete (unfold mFresh in f; unfold mFresh; allsimpl; allrw disjoint_app_r; sp)). - Case "mpcons". allsimpl. introv P M len disj f. destruct lbvars; simpl; rewrite swapLVar_app; apply app_if. + apply P; auto; try (complete (unfold mFresh in f; unfold mFresh, pFresh; allsimpl; allrw disjoint_app_r; sp)). + apply (M []); auto; try (complete (unfold mFresh in f; unfold mFresh; allsimpl; allrw disjoint_app_r; sp)). + rewrite swapLVar_subtractv. rw P; auto; try (complete (unfold mFresh in f; unfold mFresh, pFresh; allsimpl; allrw disjoint_app_r; sp)). + apply M; auto; try (complete (unfold mFresh in f; unfold mFresh; allsimpl; allrw disjoint_app_r; sp)). Qed.
imports: AlphaEquality SwapProps Eqdep_dec