proposition: Lemma alpha_preserves_free_vars : ( (forall (s : GSym G) (t1 t2 : Term s), tAlphaEq vc t1 t2 -> tfreevars vc t1 = tfreevars vc t2) * (forall (s : GSym G) (p1 p2 : Pattern s), pAlphaEq vc p1 p2 -> pfreevars vc p1 = pfreevars vc p2) * (forall a1 a2, AlphaEqAbs a1 a2 -> freevars_abs a1 = freevars_abs a2) * (forall l1 l2, lAlphaEqAbs l1 l2 -> freevars_labs l1 = freevars_labs l2) ).
proof: Proof. intros. GAlphaInd; introns Hyp; intros; try (complete (allsimpl; auto; ddeq; auto)). - Case "tnode". allsimpl. allunfold MakeAbstractionsTNode. allunfold MakeAbstractionsTNodeAux. clear Hyp. assert (forall ma : Mixture (tpRhsAugIsPat p), freevars_labs (MakeAbstractions vc ma (lBoundVars vc (bndngPatIndices p) ma)) = mfreevars vc ma (lBoundVars vc (bndngPatIndices p) ma)) as eqs. clear ma mb Hyp0. introv. remember (lBoundVars vc (bndngPatIndices p) ma); clear Heql. revert l. induction ma; introv; simpl; auto. destruct l; allsimpl. rw subtractv_nil; apply app_if; auto. apply app_if; auto. destruct l; allsimpl. rw subtractv_nil; apply app_if; auto. apply app_if; auto. repeat (rw <- eqs); auto. - Case "pnode". allsimpl. allunfold MakeAbstractionsPNode. clear Hyp. assert (forall ma : Mixture (map (fun x : GSym G => (true, x)) (ppRhsSym p)), freevars_labs (MakeAbstractions vc ma []) = mfreevars vc ma []) as eqs. clear ma mb Hyp0. introv. induction ma; introv; simpl; auto. rw subtractv_nil; apply app_if; auto. apply app_if; auto. repeat (rw <- eqs); auto. - Case "termAbs". allsimpl. allrw disjoint_app_l; repnd. rw two_as_app in Hyp1. apply tFresh_app in Hyp1; repnd. repeat (rw (fst (fst freevars_swap_eq)) in Hyp4; auto). apply eq_subtractv with (l := lbnew); auto; try (complete (apply disjoint_sym; auto)); unfold tFresh in Hyp1; unfold tFresh in Hyp6; repnd; auto; allrw disjoint_flat_map_r; pose proof (Hyp7 tmb) as h1; simpl in h1; autodimp h1 hyp; pose proof (Hyp8 tma) as h2; simpl in h2; autodimp h2 hyp. pose proof (fst (fst freevars_in_allvars) gs tma) as h. apply subset_disjoint_r with (l2 := tAllVars tma); auto. pose proof (fst (fst freevars_in_allvars) gs tmb) as h. apply subset_disjoint_r with (l2 := tAllVars tmb); auto. - Case "patAbs". allsimpl. allrw disjoint_app_l; repnd. rw two_as_app in Hyp1. apply pFresh_app in Hyp1; repnd. repeat (rw (snd (fst freevars_swap_eq)) in Hyp4; auto). apply eq_subtractv with (l := lbnew); auto; try (complete (apply disjoint_sym; auto)); unfold pFresh in Hyp1; unfold pFresh in Hyp6; repnd; auto; allrw disjoint_flat_map_r; pose proof (Hyp7 tmb) as h1; simpl in h1; autodimp h1 hyp; pose proof (Hyp8 tma) as h2; simpl in h2; autodimp h2 hyp. pose proof (snd (fst freevars_in_allvars) gs tma) as h. apply subset_disjoint_r with (l2 := pAllVars tma); auto. pose proof (snd (fst freevars_in_allvars) gs tmb) as h. apply subset_disjoint_r with (l2 := pAllVars tmb); auto. - Case "laCons". allsimpl. apply app_if; auto. Qed.
imports: AlphaEquality SwapProps Eqdep_dec