Agda2> (agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear) (agda2-info-action "*Type-checking*" "Checking Auto-Modules (Auto-Modules.agda).\n" t) (agda2-info-action "*Type-checking*" " Checking Auto.Prelude (Auto/Prelude.agda).\n" t) (agda2-info-action "*Type-checking*" " Finished Auto.Prelude.\n" t) (agda2-info-action "*Type-checking*" "Finished Auto-Modules.\n" t) (agda2-status-action "") (agda2-info-action "*All Goals*" "?0 : (P : X → Set) → ((x₁ : X) → P x₁) → Σ X P\n?1 : (A : Set) → A ∨ ¬ A\n?2 : (A : Set) → A ∨ ¬ A\n?3 : P x\n?4 : {x₁ x₂ : X} (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂)\n?5 : {x₁ x₂ x₃ : X} → Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃\n" nil) ((last . 1) . (agda2-goals-action '(0 1 2 3 4 5))) Agda2> (agda2-give-action 0 "λ P z → Σ-i x (z x)") (agda2-status-action "") (agda2-info-action "*All Goals*" "?1 : (A : Set) → A ∨ ¬ A\n?2 : (A : Set) → A ∨ ¬ A\n?3 : P x\n?4 : {x₁ x₂ : X} (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂)\n?5 : {x₁ x₂ x₃ : X} → Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃\n" nil) ((last . 1) . (agda2-goals-action '(1 2 3 4 5))) Agda2> (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\n?3 : P x\n?4 : {x₁ x₂ : X} (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂)\n?5 : {x₁ x₂ x₃ : X} → Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃\n" nil) ((last . 1) . (agda2-goals-action '(2 3 4 5))) Agda2> (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\n?4 : {x₁ x₂ : X} (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂)\n?5 : {x₁ x₂ x₃ : X} → Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃\n" nil) ((last . 1) . (agda2-goals-action '(3 4 5))) Agda2> (agda2-give-action 3 "p") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : {x₁ x₂ : X} (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂)\n?5 : {x₁ x₂ x₃ : X} → Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃\n" nil) ((last . 1) . (agda2-goals-action '(4 5))) Agda2> (agda2-give-action 4 "λ {x₁} {x₂} f z → subst (λ z₁ → Eq (f x₁) (f z₁)) z refl") (agda2-status-action "") (agda2-info-action "*All Goals*" "?5 : {x₁ x₂ x₃ : X} → Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃\n" nil) ((last . 1) . (agda2-goals-action '(5))) Agda2> (agda2-give-action 5 "λ {x₁} {x₂} {x₃} z z₁ → subst (Eq x₁) z₁ z") (agda2-status-action "") (agda2-info-action "*All Goals*" "" nil) ((last . 1) . (agda2-goals-action '())) Agda2> Agda2>