(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : X ?1 : (A × A) × (A → A) × (A → A) " nil)
((last . 1) . (agda2-goals-action '(0 1)))
(agda2-give-action 0 "φ ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?2 : Σ S (λ s₁ → P s₁ → W S P × X) " nil)
((last . 1) . (agda2-goals-action '(2 1)))
(agda2-give-action 2 "(? , ?)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?3 : S ?4 : P ?3 → W S P × X " nil)
((last . 1) . (agda2-goals-action '(3 4 1)))
(agda2-give-action 3 "s")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?4 : P s → W S P × X " nil)
((last . 1) . (agda2-goals-action '(4 1)))
(agda2-give-action 4 "(λ x → ?)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?5 : W S P × X " nil)
((last . 1) . (agda2-goals-action '(5 1)))
(agda2-give-action 5 "? , ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?6 : W S P ?7 : X " nil)
((last . 1) . (agda2-goals-action '(6 7 1)))
(agda2-give-action 6 "(k x)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?7 : X " nil)
((last . 1) . (agda2-goals-action '(7 1)))
(agda2-give-action 7 "(rec ? ?)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?8 : Σ _S_35 (λ s₁ → _P_36 s₁ → W _S_35 _P_36 × X) → X ?9 : W _S_35 _P_36 _S_35 : Set [ at 1,1-4 ] _P_36 : _S_35 → Set [ at 1,1-4 ] " nil)
((last . 1) . (agda2-goals-action '(8 9 1)))
(agda2-give-action 8 "φ")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?9 : W S (λ z → P z) " nil)
((last . 1) . (agda2-goals-action '(9 1)))
(agda2-give-action 9 "(k ?)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?10 : P s " nil)
((last . 1) . (agda2-goals-action '(10 1)))
(agda2-give-action 10 "x")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) " nil)
((last . 1) . (agda2-goals-action '(1)))
(agda2-give-action 1 "? , ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?11 : A × A ?12 : (A → A) × (A → A) " nil)
((last . 1) . (agda2-goals-action '(11 12)))
(agda2-give-action 11 "(? , ?)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?12 : (A → A) × (A → A) ?13 : A ?14 : A " nil)
((last . 1) . (agda2-goals-action '(13 14 12)))
(agda2-give-action 12 "(? , ?)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?13 : A ?14 : A ?15 : A → A ?16 : A → A " nil)
((last . 1) . (agda2-goals-action '(13 14 15 16)))
(agda2-give-action 15 "(λ x → ?)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?13 : A ?14 : A ?16 : A → A ?17 : A " nil)
((last . 1) . (agda2-goals-action '(13 14 17 16)))
(agda2-give-action 16 "(λ x → ?)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?13 : A ?14 : A ?17 : A ?18 : A " nil)
((last . 1) . (agda2-goals-action '(13 14 17 18)))
