```module Orn.Reornament.Examples.Iterative (A B C : Set) where

open import Data.Unit
open import Data.Nat
open import Data.Bool
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Level renaming (zero to zeroL ; suc to sucL)

open import Logic.Logic
open import Logic.IProp
open Logic.IProp.Applicative {zeroL}

open import IDesc.IDesc
open import IDesc.Fixpoint

open import Orn.Ornament
open import Orn.Reornament

-- Paper: Remark 4.33

test : func ⊤ ⊤
test = mk (λ x → `Σ A (λ a →
`Π B λ b →
`Σ Bool λ x →
`var tt))

forget : ℕ → ⊤
forget n = tt

testO : orn test forget forget
testO = mk (λ n → `Σ (λ a →
insert C (λ c →
`Π (λ b →
deleteΣ true
(`var (inv (ℕ.suc n)))))))

postulate
a : A
b : B
c : C
n : ℕ
x : Bool
xs : μ test tt

reorn1 : orn ⟦ testO ⟧orn proj₁ proj₁
reorn1 = ⌈ testO ⌉

reorn1O : Orn proj₁ (func.out ⟦ testO ⟧orn n)
reorn1O = orn.out reorn1 (n , ⟨ a , (λ _ → x , xs) ⟩)

{-
reorn1 (n , ⟨ a , (λ _ → x , xs) ⟩ )  ↝
deleteΣ a
(`Σ (λ c →
`Π (λ b →
insert (x ≡ true) (λ q →
`var (inv (ℕ.suc n , xs))))))
-}

reorn2 : orn ⟦ reorn1 ⟧orn proj₁ proj₁
reorn2 = ⌈ reorn1 ⌉

postulate
a' : A
xs⁺ : μ ⟦ testO ⟧orn (ℕ.suc n)

reorn2O : Orn proj₁ (func.out ⟦ reorn1 ⟧orn (n , ⟨ a , (λ _ → x , xs) ⟩))
reorn2O = orn.out reorn2 ((n , ⟨ a , (λ _ → x , xs) ⟩) , ⟨ a' , c , (λ _ → xs⁺) ⟩)

{-
reorn2 ((n , ⟨ a , (λ _ → x , xs) ⟩) , ⟨ a , c , (λ _ → xs⁺) ⟩ ) ↝
insert (a' ≡ a) (λ qa →
deleteΣ c
(`Π (λ b →
`Σ (λ qx →
`var (inv ((ℕ.suc n , xs) , xs⁺ b))))))
-}

reorn3 : orn ⟦ reorn2 ⟧orn proj₁ proj₁
reorn3 = ⌈ reorn2 ⌉

postulate
c' : C
xs⁺⁺ : μ ⟦ reorn1 ⟧orn (ℕ.suc n , xs)

reorn3O : Orn proj₁  (func.out ⟦ reorn2 ⟧orn ((n , ⟨ a , (λ _ → true , xs) ⟩) , ⟨ (a , (c , (λ _ → xs⁺))) ⟩))
reorn3O = orn.out reorn3 (((n , ⟨ a , (λ _ → true , xs) ⟩) , ⟨ a , c , (λ _ → xs⁺) ⟩) , ⟨ (c' , (λ b → refl , xs⁺⁺)) ⟩)

{-
reorn3 (((n , ⟨ a , (λ _ → true , xs) ⟩) , ⟨ a , c , (λ _ → xs⁺) ⟩ ) , ⟨ c' , λ b → refl , xs⁺⁺ ⟩ ) ↝
`Σ (λ q₁ →
insert (c' ≡ c) (λ q₂ →
`Π (λ b →
deleteΣ refl
(`var (inv (((ℕ.suc n , xs) , xs⁺ b , xs⁺⁺ b)))))))
-}

lemma : ∀{i₁ i₂ i₃ i₄} → (x y : μ ⟦ reorn3 ⟧orn (((i₁ , i₂) , i₃) , i₄)) → ⊢ x ≡ y
lemma {i₂ = ⟨ i₂₁ , i₂₂ ⟩}
{⟨ .i₂₁ , i₄₁ , i₃₃ ⟩}
{⟨ .i₄₁ , i₄₂ ⟩}
⟨ refl , refl , x ⟩
⟨ refl , refl , y ⟩ = cong (λ x → ⟨ refl , refl , x ⟩) <\$>
extensionality (λ b → lemma (x b) (y b))
```