- | RId a => let case_RId := tt in ga_id _ _ _ _ _
- | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
- | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
- | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
- | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
- | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
- | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
- | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
- | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
- | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
- | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
- | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
- | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
+ | AId a => let case_AId := tt in ga_id _ _ _ _ _
+ | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _
+ | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _
+ | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _
+ | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
+ | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
+ | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
+ | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _
+ | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _
+ | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _
+ | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
+ | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
+ | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)