proposition: Lemma EquivariantSSubstAux : (forall {gs : GSym G}, EquiVariantFn2 (@tSwap _ vc gs) (@swapSub G vc) (@tSwap _ vc gs) (@tSSubstAux _ _ _)) * (forall (gs : GSym G), EquiVariantFn2 (@pSwap _ vc gs) (@swapSub G vc) (@pSwap _ vc gs) (@pSSubstAux _ _ _)) * (forall (lgs : list (bool * GSym G)), EquiVariantFn3 (@mSwap _ vc lgs) (fun x s => swapLLVar s x) (@swapSub G vc) (@mSwap _ vc lgs) (@mSSubstAux _ _ _)).
proof: Proof. GInduction; introns Hyp; allsimpl; cpx; try (intros; f_equal; cpx; fail). - Case "vleaf". intros. simpl. destruct_head_match; allsimpl; cpx; [|f_equal;destruct_head_match; cpx]. destruct e. allsimpl. rename tb into sub. unfold ALFindDef. assert (injective_fun (swapVar sw)) by (introv Hq; apply swapVarInj in Hq; trivial). DALFindC fsv. + unfold swapSub. erewrite ALFindMapSome; eauto. + unfold swapSub. erewrite ALFindMapNone; eauto. simpl. rewrite DeqTrue. simpl. refl. - Case "tnode". intros. simpl. f_equal. rewrite lBoundVars_swap. apply Hyp. - Case "pnode". intros. simpl. f_equal. apply Hyp. - Case "mtcons". intros. rename tb into lvb. destruct lvb; allsimpl; f_equal; cpx; [rw Hyp0; simpl; cpx|]. rw Hyp. f_equal. symmetry. apply swapSubFilterCommute. - Case "mpcons". intros. rename tb into lvb. destruct lvb; allsimpl; f_equal; cpx; [rw Hyp0; simpl; cpx|]. rw Hyp. f_equal. symmetry. apply swapSubFilterCommute. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux