Agda2> (agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear) (agda2-info-action "*Type-checking*" "Checking Auto-BasicLogic (Auto-BasicLogic.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-BasicLogic.\n" t) (agda2-status-action "") (agda2-info-action "*All Goals*" "?0 : (A : Set) → A → A\n?1 : (A B : Set) → A → (A → B) → B\n?2 : (A B : Set) → A ∧ B → B ∧ A\n?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C)\n?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?8 : (A : Set) → A → ¬ (¬ A)\n?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A\n?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A\n?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A\n?12 : {X : Set} {P Q : X → Set} →\n((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17))) Agda2> (agda2-give-action 0 "λ A z → z") (agda2-status-action "") (agda2-info-action "*All Goals*" "?1 : (A B : Set) → A → (A → B) → B\n?2 : (A B : Set) → A ∧ B → B ∧ A\n?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C)\n?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?8 : (A : Set) → A → ¬ (¬ A)\n?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A\n?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A\n?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A\n?12 : {X : Set} {P Q : X → Set} →\n((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17))) Agda2> (agda2-give-action 1 "λ A B z z₁ → z₁ z") (agda2-status-action "") (agda2-info-action "*All Goals*" "?2 : (A B : Set) → A ∧ B → B ∧ A\n?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C)\n?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?8 : (A : Set) → A → ¬ (¬ A)\n?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A\n?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A\n?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A\n?12 : {X : Set} {P Q : X → Set} →\n((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17))) Agda2> (agda2-give-action 2 "λ A B z → ∧-i (_∧_.snd z) (_∧_.fst z)") (agda2-status-action "") (agda2-info-action "*All Goals*" "?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C)\n?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?8 : (A : Set) → A → ¬ (¬ A)\n?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A\n?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A\n?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A\n?12 : {X : Set} {P Q : X → Set} →\n((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(3 4 5 6 7 8 9 10 11 12 13 14 15 16 17))) Agda2> (agda2-give-action 3 "λ A B C z →\n ∧-i (_∧_.fst (_∧_.fst z)) (∧-i (_∧_.snd (_∧_.fst z)) (_∧_.snd z))") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?8 : (A : Set) → A → ¬ (¬ A)\n?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A\n?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A\n?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A\n?12 : {X : Set} {P Q : X → Set} →\n((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17))) Agda2> ((last . 2) . (agda2-make-case-action '("h4 A B C (∨-i₁ x) h₁ h₂ = h₁ x" "h4 A B C (∨-i₂ x) h₁ h₂ = h₂ x"))) ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17))) Agda2> ((last . 2) . (agda2-make-case-action '("h5 A B (∨-i₁ x) = ∨-i₂ x" "h5 A B (∨-i₂ x) = ∨-i₁ x"))) ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17))) Agda2> ((last . 2) . (agda2-make-case-action '("h6 A B C (∨-i₁ (∨-i₁ x)) = ∨-i₁ x" "h6 A B C (∨-i₁ (∨-i₂ x)) = ∨-i₂ (∨-i₁ x)" "h6 A B C (∨-i₂ x) = ∨-i₂ (∨-i₂ x)"))) ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17))) Agda2> ((last . 2) . (agda2-make-case-action '("h7 A ()"))) ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17))) Agda2> (agda2-give-action 8 "λ A z z₁ → z₁ z") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A\n?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A\n?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A\n?12 : {X : Set} {P Q : X → Set} →\n((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 9 10 11 12 13 14 15 16 17))) Agda2> (agda2-give-action 9 "λ A z z₁ → z (λ z₂ → z₂ z₁)") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A\n?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A\n?12 : {X : Set} {P Q : X → Set} →\n((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 10 11 12 13 14 15 16 17))) Agda2> (agda2-give-action 10 "λ z A →\n z (A ∨ ((x : A) → ⊥)) (λ z₁ → z₁ (∨-i₂ (λ x → z₁ (∨-i₁ x))))") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A\n?12 : {X : Set} {P Q : X → Set} →\n((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 11 12 13 14 15 16 17))) Agda2> (agda2-give-action 11 "λ z A z₁ →\n ∨-e A ((x : A) → ⊥) A (z A) (λ z₂ → z₂) (λ z₂ → ⊥-e A (z₁ z₂))") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?12 : {X : Set} {P Q : X → Set} →\n((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 12 13 14 15 16 17))) Agda2> (agda2-give-action 12 "λ {X} {P} {Q} z → ∧-i (λ x → _∧_.fst (z x)) (λ x → _∧_.snd (z x))") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?13 : {X : Set} {P Q : X → Set} →\n((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 13 14 15 16 17))) Agda2> (agda2-give-action 13 "λ {X} {P} {Q} z x → ∧-i (_∧_.fst z x) (_∧_.snd z x)") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?14 : {X : Set} → X → Σ X (λ x → ⊤)\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 14 15 16 17))) Agda2> (agda2-give-action 14 "λ {X} x → Σ-i x (record {})") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?15 : {X : Set} → Σ (X → X) (λ x → ⊤)\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 15 16 17))) Agda2> (agda2-give-action 15 "λ {X} → Σ-i (λ x → x) (record {})") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 16 17))) Agda2> (agda2-give-action 16 "λ {X} {P} → Σ-i (λ x → x) (λ x x₁ → x₁)") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n?17 : Σ A (λ x → Drink x → Π A Drink)\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7 17))) Agda2> (agda2-give-action 17 "RAA (Σ A (λ z → (x : Drink z) → Π A Drink))\n(λ z →\n z\n (Σ-i a\n (λ x →\n fun\n (λ a₁ →\n RAA (Drink a₁)\n (λ z₁ →\n z (Σ-i a₁ (λ x₁ → fun (λ a₂ → RAA (Drink a₂) (λ _ → z₁ x₁)))))))))") (agda2-status-action "") (agda2-info-action "*All Goals*" "?4 : C\n?5 : B ∨ A\n?6 : A ∨ (B ∨ C)\n?7 : A\n" nil) ((last . 1) . (agda2-goals-action '(4 5 6 7))) Agda2> Agda2>