--- a/src/Polynominal.agda	Sun May 16 23:38:00 2021 +0900
+++ b/src/Polynominal.agda	Mon May 17 01:19:00 2021 +0900
@@ -82,6 +82,7 @@
        phi  : φ x {b} {c} f                                      -- construction of f
        nf : (fp : φ x {b} {c} f) → xnef x fp
 
+
   -- since we have A[x] now, we can proceed the proof on p.64 in some possible future
 
   --
@@ -234,12 +235,10 @@
                f' ∙  < π , π' >  ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
                f' ∙  id1 A _ ≈⟨ idR ⟩
                f' ∎  )  where
-                   --  (phi : φ x f) → xnef x phi
-                   xff :  ((fp : φ x f) → xnef x fp)  → (g : Hom A b a)  → (gp : φ x g)  → xnef x gp
-                   xff = {!!}
-                   xf :  (fp : φ x (x ∙ ○ b)) → xnef x fp
-                   xf = {!!}
-                   u2 : k x {x ∙ ○ b} (i _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _) > 
+                   -- x ∙ ○ b is clearly Polynominal, but our xnef is too strong to prove it
+                   postulate 
+                      xf : {a b : Obj A} → { x : Hom A １ a } →  (fp : φ x (x ∙ ○ b)) → xnef x fp
+                   u2 : k x {x ∙ ○ b} (i _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _) >  --  (x ∙ (○ b)) ∙ π' ≈ π ∙ < π , (○ b) ∙ π' >
                    u2 = ki x (x ∙ ○ b) (iv ii (i _)) xf
 
   -- functional completeness ε form