proposition: Lemma swapBndngVarsCommute: ( forall (s : GSym G) (nt : Term s), True) * ( forall (s : GSym G) (pt : Pattern s) (sw : Swapping vc), swapLVar sw (pBndngVars vc pt) = pBndngVars vc (pSwap pt sw) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l) (sw : Swapping vc) (nn : nat), swapLVar sw (getBVarsNth vc m nn) = @getBVarsNth _ vc _ (mSwap m sw) nn ).
proof: Proof. GInduction; allsimpl; introns Hyp; intros; cpx; [ | | | ]. - Case "pvleaf". rewrite DeqSym. symmetry. rewrite DeqSym. destruct_head_match; subst; auto. - Case "pnode". simpl. simpl pBndngVars. rewrite mBndngVarsAsNth. rewrite mBndngVarsAsNth. autorewrite with fast. unfold swapLVar. unfold swapLVar in Hyp. rw map_flat_map. apply eq_flat_maps. intros nn Hin. unfold compose. trivial. - simpl. destruct nn; auto. - simpl. destruct nn; auto. Qed.
imports: Swap