proposition: Theorem bindersSSubstAuxNoCnange: ( forall (s : GSym G) (nt : Term s), True) * ( forall (s : GSym G) (pt : Pattern s) (sub : SSubstitution vc), pBndngVars vc pt = pBndngVars vc (pSSubstAux pt sub) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l) (sub : SSubstitution vc) (lbv : list (list (vType vc))) (nn : nat), getBVarsNth vc m nn = @getBVarsNth _ vc _ (mSSubstAux m lbv sub) nn ).
proof: Proof. 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. + simpl. destruct lbv; cpx; simpl. + destruct lbv; simpl; cpx; simpl; eapply IHm; eauto. - simpl. destruct nn. + simpl. destruct lbv; cpx; simpl. + destruct lbv; simpl; cpx; simpl; eapply IHm; eauto. Qed.
imports: Term AssociationList