proposition: Theorem lbShallowNoChange: forall {G : CFGV} {vc : VarSym G}, ( forall (s : GSym G) (nt : Term s), True) * ( forall (s : GSym G) (pt : Pattern s) (lvA : list (vType vc)), pBndngVars vc pt = pBndngVars vc (pRenAlpha pt lvA) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l) (lvA : list (vType vc)) (nn : nat), getBVarsNth vc m nn = @getBVarsNth _ vc _ (mRenAlpha m lvA) nn ).
proof: Proof. intros. GInduction; allsimpl; introns Hyp; intros; cpx;[ | | ]. - Case "pnode". simpl. simpl pBndngVars. rewrite mBndngVarsAsNth. rewrite mBndngVarsAsNth. autorewrite with fast. apply eq_flat_maps. intros nn Hin. cpx. - simpl. destruct nn; cpx. - simpl. destruct nn; cpx. Qed.
imports: AlphaEqProps Omega