exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
branch_tac;
pos_tac [3]; exact_tac t;
shift_tac; pos_tac [2]; skip_tac;
exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
branch_tac;
pos_tac [3]; exact_tac t;
shift_tac; pos_tac [2]; skip_tac;