
/* Tatica extendVarScope */

\tbegin
\ttactic extendVarScope()  \def


\tappliesto (AIn \circseq (\circmu X \circspot (\circvar d : \nat \circspot  A) \circseq EC))
        \tdo
            (\tskip \semibox(
							(\mubox (\tlaw Sequence_Unit_part_2() \tsemi \tlaw var_exp_seq() \tsemi \varbox (\tlaw Sequence_Unit_part_2() )))
							\tsemi \tlaw Var_Exp_Rec() \tsemi \tlaw Sequence_Unit_part_1()))
							\tsemi \tlaw var_exp_seq() \tsemi \varbox (\tskip \semibox \tlaw Sequence_Unit_part_1())
\tend	
						