--- a/src/Polynominal.agda	Sun May 16 13:17:22 2021 +0900
+++ b/src/Polynominal.agda	Sun May 16 13:46:39 2021 +0900
@@ -234,21 +234,10 @@
                f' ∙  < π , π' >  ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
                f' ∙  id1 A _ ≈⟨ idR ⟩
                f' ∎  )  where
-                   u1 : x ∙ ○ b ≈ ( x  ∙ ○ _ ) ∙ ( < π , k x {○ b} (i _) >  ∙ < x ∙ ○ b , id1 A b > )
-                   u1 = begin
-                     x ∙ ○ b ≈↑⟨ cdr e2 ⟩
-                     x ∙ ( ○ _ ∙ _ )  ≈⟨ assoc ⟩
-                     ( x  ∙ ○ _ ) ∙ ( < π , k x {○ b} (i _) >  ∙ < x ∙ ○ b , id1 A b > )  ∎  
+                   xf :  (fp : φ x (x ∙ ○ b)) → xnef x fp
+                   xf = {!!}
                    u2 : k x {x ∙ ○ b} (i _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _) > 
-                   u2 = begin
-                     k x {x ∙ ○ b} (i _) ≈↑⟨ assoc ⟩     --- (x ∙ ○ b) ∙ π'
-                     x ∙ (○ _ ∙ π') ≈⟨ cdr e2 ⟩
-                     x ∙ ○ _ ≈↑⟨ IsCCC.e3a isCCC ⟩
-                     k x {x} ii ∙ < ( x ∙ ○ _ )  ,  k x {○ b} (i _) >  ≈⟨ {!!} ⟩
-                     k x {x} ii ∙ < π ∙ < x ∙ {!!} , id1 A _ >  ,  k x {○ b} (i _) >  ≈⟨ {!!} ⟩
-                     k x {x} ii ∙ < π ∙ id1 A _  ,  k x {○ b} (i _) >  ≈⟨ {!!} ⟩
-                     k x {x} ii ∙ < π ,             k x {○ b} (i _) > ∎  
-
+                   u2 = ki x (x ∙ ○ b) (iv ii (i _)) xf
 
   -- functional completeness ε form
   --