%{}%
elem : type.
z : elem.

list : type.

nil : list.
cons : elem -> list -> list.

%block bl_elem : block {x : elem}.

id : list -> list -> type.
refl : id L L.

fillx : (elem -> list) -> list -> type.
fillx1 : fillx ([x] nil) nil.
fillx2 : fillx ([x] cons x (L₁ x)) L₂ 
         <- fillx ([x] L₁ x) L₂.
fillx3 : fillx ([x] cons Y (L₁ x)) (cons Y L₂)
         <- fillx ([x] L₁ x) L₂.

fill : {D : elem -> list} fillx D E -> type.
- : fill ([x] nil) fillx1.
- : fill ([x] cons x (D x)) (fillx2 D⟦·⟧) <- fill D D⟦·⟧.
- : fill ([x] cons Y (D x)) (fillx3 D⟦·⟧) <- fill D D⟦·⟧.
%mode fill +D -D⟦·⟧.
%worlds (bl_elem) (fill _ _).
%total D (fill D _).

fillR : (elem -> list) -> elem -> list -> type.
fillR0 : fillR ([x] L x) R (L R).

fillR-cons-cong : {Rh} 
                   fillR L R LR
                   -> fillR ([x] (cons Rh (L x))) R (cons Rh LR)
                   -> type.
%mode fillR-cons-cong +X1 +X2 -X3.
- : fillR-cons-cong _ fillR0 fillR0.
%worlds (bl_elem) (fillR-cons-cong _ _ _).
%total {} (fillR-cons-cong _ _ _).

void : type.
%worlds () (void).

fill-nil-contra : fillR ([x] nil) R₂ (cons R₁ L2)
                   -> void
                   -> type.
%mode fill-nil-contra +X1 -X2.
%worlds (bl_elem) (fill-nil-contra _ _).
%total {} (fill-nil-contra _ _).

abort/fillR : {L}{R}{LR} void -> fillR L R LR -> type.
%mode abort/fillR +X1 +X2 +X3 +X4 -X5.
%worlds (bl_elem) (abort/fillR _ _ _ _ _).
%total {} (abort/fillR _ _ _ _ _).

abort/fillx : {L}{Lx} void -> fillx L Lx -> type.
%mode abort/fillx +X1 +X3 +X4 -X5.
%worlds (bl_elem) (abort/fillx _ _ _ _).
%total {} (abort/fillx _ _ _ _).

fillRx2 : fillR L R LR
           -> fillR ([x] cons x (L x)) R (cons R LR)
           -> type.
%mode fillRx2 +X1 -X2.
- : fillRx2 fillR0 fillR0.
%worlds (bl_elem) (fillRx2 _ _).
%total {} (fillRx2 _ _).

thm' : {D□R : elem -> list}
      {D·□ : elem -> list}
      fillR ([x] D·□ x) R D·R
   -> fillx ([x] D□R x) D·R
   -> {D□□ : elem -> elem -> list}
      ({y} fillx ([x] D□□ x y) (D·□ y))
   -> ({x} fillR ([y] D□□ x y) R (D□R x))
   -> type. 
%abbrev thm : {D□R : elem -> list}
      {D·□ : elem -> list}
      fillx ([x] D□R x) D·R
   -> fillR ([x] D·□ x) R D·R
   -> {D□□ : elem -> elem -> list}
      ({y} fillx ([x] D□□ x y) (D·□ y))
   -> ({x} fillR ([y] D□□ x y) R (D□R x))
   -> type = [x1] [x2] [x3] [x4] [x5] [x6] [x7] thm' x1 x2 x4 x3 x5 x6 x7. 


- : thm ([x] nil) ([y] nil) fillx1 F1 
     ([x][y] nil) ([x] fillx1) ([x] fillR0).
- : thm ([x] cons x (L1 x)) ([y] L2 y) (fillx2 F1) fillR0 
     ([x][y] cons x (L x y)) 
     ([y] fillx2 (B y)) 
     ([x] C' x : fillR ([y] cons x (L x y)) R (cons x (L1 x)))
     <- thm L1 L2 F1 fillR0 
        ([x][y] L x y) 
        ([y] B y : fillx ([x] L x y) (L2 y))
        ([x] C x : fillR ([y] L x y) R (L1 x))
     <- ({x:elem} fillR-cons-cong x (C x) (C' x)).

- : thm ([x] cons R₁ (L1 x)) ([x] nil) (fillx3 F3) 
     (F1 : fillR ([x] nil) R₂ (cons R₁ L2'))
     ([x] [y] nil) %% garbage 
     B
     C
     <- fill-nil-contra F1 XX
     <- ({x} abort/fillx _ _ XX (B x))
     <- ({x} abort/fillR _ _ _ XX (C x)).

- : thm ([x] cons R₁ (L1 x)) ([x] cons R₁ (L2 x)) (fillx3 F1) 
     (fillR0 : fillR ([x] cons R₁ (L2 x)) R₂ (cons R₁ (L2 R₂)))
     ([x][y] cons R₁ (L x y)) 
     ([y] fillx3 (F1' y)) 
     ([x] B' x : fillR ([y:elem] cons R₁ (L x y)) R₂ (cons R₁ (L1 x)))
     <- thm L1 L2 F1 fillR0 ([x][y] L x y) 
        ([y] F1' y : fillx ([x] L x y) (L2 y))
        ([x] B x : fillR ([x1:elem] L x x1) R₂ (L1 x))
     <- ({x:elem} fillR-cons-cong R₁ (B x) (B' x)).

- : thm ([x] cons R₁ (L1 x)) ([x] cons x (L2 x)) (fillx3 F1) 
     (fillR0 : fillR ([x] cons x (L2 x)) R₁ (cons R₁ (L2 R₁)))
     ([x][y] cons y (L x y))
     ([y] (fillx3 (F1' y)))
     ([x] B' x : fillR ([y] cons y (L x y)) R₁ (cons R₁ (L1 x)))
     <- thm L1 L2 F1 fillR0 ([x][y] L x y) 
        ([y] F1' y)
        ([x] B x : fillR ([y] L x y) R₁ (L1 x))
     <- ({x} fillRx2 (B x) (B' x)).

%worlds (bl_elem) (thm' _ _ _ _ _ _ _).
%covers thm' +A +B +C +D -E -F -G.
%mode thm' +A +B +C +D -E -F -G.
%total D (thm' D _ _ _ _ _ _).

com·· : {D□□ : elem -> elem -> list} 
         ({y} fillx ([x] D□□ x y) (D·□ y))
      -> ({x} fillx ([y] D□□ x y) (D□· x))
      -> (fillx ([y] D·□ y) D··)
      -> (fillx ([x] D□· x) D··)
      -> type.
- : com·· ([x][y] nil) ([y] fillx1) ([x] fillx1) fillx1 fillx1.
- : com·· ([x][y] cons E (L x y))
     ([y] fillx3 (Fx y)) ([x] fillx3 (Fy x)) (fillx3 Fxy) (fillx3 Fyx)
     <- com·· L Fx Fy Fxy Fyx.
- : com·· ([x][y] cons x (L x y)) 
     ([y] fillx2 (Fx y)) ([x] fillx3 (Fy x)) Fxy (fillx2 Fyx)
     <- com·· L Fx Fy Fxy Fyx.
- : com·· ([x][y] cons y (L x y))
     ([y] fillx3 (Fx y)) ([x] fillx2 (Fy x)) (fillx2 Fxy) Fyx
     <- com·· L Fx Fy Fxy Fyx.
%mode com·· +A +B +C +D -E.
%worlds (bl_elem) (com·· _ _ _ _ _).
%total T (com·· T _ _ _ _).

comR· : {D□□ : elem -> elem -> list}
         ({x} fillx ([y] D□□ x y) (D□· x))
      -> (fillx ([y] D□□ R y) (D□· R))
      -> type.
- : comR· ([x][y] nil) ([x] fillx1) fillx1.
- : comR· ([x][y] cons E (L x y)) ([x] fillx3 (Fy x)) (fillx3 Fxy)
     <- comR· L Fy Fxy.
- : comR· ([x][y] cons x (L x y)) ([x] fillx3 (Fy x)) (fillx3 Fxy)
     <- comR· L Fy Fxy.
- : comR· ([x][y] cons y (L x y)) ([x] fillx2 (Fy x)) (fillx2 Fxy)
     <- comR· L Fy Fxy.
%mode +{D□·:elem -> list} +{A:elem -> elem -> list} +{R:elem}
   +{C:{x:elem} fillx ([y:elem] A x y) (D□· x)}
   -{E:fillx ([y:elem] A R y) (D□· R)} (comR· A C E).
%worlds (bl_elem) (comR· _ _ _).
%total T (comR· T _ _).

filleq : {R₁} ({x:elem} fillR ([y] D□□ x y) R₂ (D□R x))
          -> fillR ([x] D□□ R₁ x) R₂ (D□R R₁)
          -> type.
- : filleq _ ([x] fillR0) fillR0.
%worlds (bl_elem) (filleq _ _ _).
%mode filleq +A +C -B.
%total {} (filleq _ _ _).

holeswap : {R₁}
           {R₂}
           {D□R : elem -> list}
           {D·□ : elem -> list}
           fillR D□R R₁ DRR
        -> fillx D□R D·R
        -> fillR D·□ R₂ D·R
        -> fillx D·□ D··
        -> {D□· : elem -> list}
           {DR□ : elem -> list}
           fillx D□· D··
        -> fillR D□· R₁ DR·
        -> fillx DR□ DR·
        -> fillR DR□ R₂ DRR
        -> type.

- : holeswap R₁ R₂ D□R D·□ fillR0 D□R⟦x⟧ fillR0 D·□⟦y⟧ 
     D□· ([y] D□□ R₁ y) D□·⟦x⟧ fillR0 DR□⟦y⟧ D□R⟦R⟧
     <- thm' D□R D·□ fillR0 D□R⟦x⟧ D□□
        ([y] D□□⟦x⟧ y : fillx ([x] D□□ x y) (D·□ y)) 
        ([x] D□□⟦R⟧ x : fillR ([y] D□□ x y) R₂ (D□R x))
     <- ({x} fill ([y] D□□ x y) (D□□⟦y⟧ x : fillx ([y] D□□ x y) (D□· x)))
     <- com·· D□□ D□□⟦x⟧ D□□⟦y⟧ D·□⟦y⟧ D□·⟦x⟧
     <- comR· D□□ D□□⟦y⟧ DR□⟦y⟧
     <- filleq _ D□□⟦R⟧ D□R⟦R⟧.

%worlds (bl_elem) (holeswap _ _ _ _ _ _ _ _ _ _ _ _ _ _).
%mode holeswap +A +B +C +D +E +F +G +H -I -K -L -M -N -O.
%total {} (holeswap _ _ _ _ _ _ _ _ _ _ _ _ _ _).