(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : (P : X → Set) → ((x₁ : X) → P x₁) → Σ X P ?1 : (A : Set) → A ∨ ¬ A ?2 : (A : Set) → A ∨ ¬ A ?3 : P x ?4 : (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂) ?5 : Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃ " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
(agda2-give-action 0 "λ P z → Σ-i x (z x)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A : Set) → A ∨ ¬ A ?2 : (A : Set) → A ∨ ¬ A ?3 : P x ?4 : (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂) ?5 : Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃ " nil)
((last . 1) . (agda2-goals-action '(1 2 3 4 5)))
(agda2-give-action 1 "λ A → RAA (A ∨ ((x : A) → ⊥)) (λ z → z (∨-i₂ (λ x → z (∨-i₁ x))))")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?2 : (A : Set) → A ∨ ¬ A ?3 : P x ?4 : (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂) ?5 : Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃ " nil)
((last . 1) . (agda2-goals-action '(2 3 4 5)))
(agda2-give-action 2 "λ A → RAA (A ∨ ((x : A) → ⊥)) (λ z → z (∨-i₂ (λ x → z (∨-i₁ x))))")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?3 : P x ?4 : (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂) ?5 : Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃ " nil)
((last . 1) . (agda2-goals-action '(3 4 5)))
(agda2-give-action 3 "p")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂) ?5 : Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃ " nil)
((last . 1) . (agda2-goals-action '(4 5)))
(agda2-give-action 4 "λ f z → subst (λ z₁ → Eq (f x₁) (f z₁)) z refl")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?5 : Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃ " nil)
((last . 1) . (agda2-goals-action '(5)))
(agda2-give-action 5 "λ z z₁ → subst (Eq x₁) z₁ z")
(agda2-status-action "")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
