(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : A → A ?1 : A → A ?2 : B ?3 : Set _a_24 _18 : Set _a_24 [ at Issue2749-2.agda:21,11-12 ] _a_24 : Agda.Primitive.Level [ at Issue2749-2.agda:21,19-20 ] " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3)))
(agda2-give-action 0 "λ x → ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : A → A ?2 : B ?3 : Set _a_24 ?4 : A _18 : Set _a_24 [ at Issue2749-2.agda:21,11-12 ] _a_24 : Agda.Primitive.Level [ at Issue2749-2.agda:21,19-20 ] " nil)
((last . 1) . (agda2-goals-action '(4 1 2 3)))
(agda2-status-action "ShowImplicit")
((last . 2) . (agda2-make-case-action '("it {A} ⦃ a ⦄ x = ?")))
((last . 1) . (agda2-goals-action '(4 1 2 3)))
(agda2-status-action "")
((last . 2) . (agda2-make-case-action '("left (mkB b₁ b₂) = ?")))
((last . 1) . (agda2-goals-action '(4 1 2 3)))
((last . 2) . (agda2-solveAll-action '(3 "∀ (m : ?) n → m ≡ n")))
((last . 1) . (agda2-goals-action '(4 1 2 3)))
