text:
open import Relation.Binary.Core

module PLRTree.Push.Complete {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_)  where

open import Data.Sum
open import Induction.WellFounded
open import PLRTree {A}
open import PLRTree.Drop _≤_ tot≤
open import PLRTree.Complete {A}
open import PLRTree.Equality {A}
open import PLRTree.Equality.Properties {A}
open import PLRTree.Order {A}
open import PLRTree.Order.Properties {A}

mutual
  lemma-≃-push : {t t' : PLRTree} → t ≃ t' → (acc : Acc _≺_ t) → t ≃ push t acc
  lemma-≃-push ≃lf _ = ≃lf
  lemma-≃-push (≃nd x x' ≃lf ≃lf ≃lf) _ = ≃nd x x ≃lf ≃lf ≃lf
  lemma-≃-push (≃nd x x' (≃nd {l₁} {r₁} {l₂} {r₂} x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) l'≃r' (≃nd .x₁ x'₁ _ l'₁≃r'₁ l₁≃l'₁)) (acc rs)
      with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
  ... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ =
             let l₁≃l₁ = lemma-≃-≃ l₁≃r₁
             in ≃nd x x (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) (≃nd x₁ x₁ l₁≃r₁ l₁≃r₁ l₁≃l₁)
  ... | inj₁ x≤x₁ | inj₂ x₂≤x | _ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁≃x₂l₂r₂ = lemma-≃-push  (sym≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂)) acc-xl₂r₂ ;
                  x₁l₁r₁≃push-xl₂r₂ = trans≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂) push-xl₁r₁≃x₂l₂r₂ ;
                  x₁l₁r₁≃x₁l₁r₁ = lemma-≃-≃ (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂)
             in ≃nd x x₂ (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) x₁l₁r₁≃push-xl₂r₂ x₁l₁r₁≃x₁l₁r₁
  ... | inj₂ x₁≤x | inj₁ x≤x₂ | _ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁≃x₂l₂r₂ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) ;
                  l₁≃l₁ = lemma-≃-≃ l₁≃r₁ ;
                  x₁l₁r₁≃xl₁r₁ = ≃nd x₁ x l₁≃r₁ l₁≃r₁ l₁≃l₁ ;
                  xl₁r₁≃push-xl₁r₁ = lemma-≃-push (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁ ;
                  x₁l₁r₁≃push-xl₁r₁ = trans≃ x₁l₁r₁≃xl₁r₁ xl₁r₁≃push-xl₁r₁
             in ≃nd x x₁ (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) push-xl₁r₁≃x₂l₂r₂ x₁l₁r₁≃push-xl₁r₁
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁≃x₂l₂r₂ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) ;
                  l₁≃l₁ = lemma-≃-≃ l₁≃r₁ ;
                  x₁l₁r₁≃xl₁r₁ = ≃nd x₁ x l₁≃r₁ l₁≃r₁ l₁≃l₁ ;
                  xl₁r₁≃push-xl₁r₁ = lemma-≃-push (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁ ;
                  x₁l₁r₁≃push-xl₁r₁ = trans≃ x₁l₁r₁≃xl₁r₁ xl₁r₁≃push-xl₁r₁
             in ≃nd x x₁ (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) push-xl₁r₁≃x₂l₂r₂ x₁l₁r₁≃push-xl₁r₁
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁≃x₂l₂r₂ = lemma-≃-push  (sym≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂)) acc-xl₂r₂ ;
                  x₁l₁r₁≃push-xl₂r₂ = trans≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂) push-xl₁r₁≃x₂l₂r₂ ;
                  x₁l₁r₁≃x₁l₁r₁ = lemma-≃-≃ (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂)
             in ≃nd x x₂ (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) x₁l₁r₁≃push-xl₂r₂ x₁l₁r₁≃x₁l₁r₁

  lemma-push-≃ : {t t' : PLRTree} → t ≃ t' → (acc : Acc _≺_ t) → push t acc ≃ t
  lemma-push-≃ t≃t' at = sym≃ (lemma-≃-push t≃t' at)

lemma-push-⋗ : {t t' : PLRTree} → t ⋗ t' → (acc : Acc _≺_ t) → push t acc ⋗ t'
lemma-push-⋗ (⋗lf x) _ = ⋗lf x
lemma-push-⋗ (⋗nd _ _ ≃lf _ ()) _
lemma-push-⋗ (⋗nd x x' (≃nd x₁ x₂ ≃lf ≃lf ≃lf) ≃lf (⋗lf .x₁)) (acc rs)
    with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ = ⋗nd x x' (≃nd x₁ x₂ ≃lf ≃lf ≃lf) ≃lf (⋗lf x₁)
... | inj₁ x≤x₁ | inj₂ x₂≤x | _ = ⋗nd x₂ x' (≃nd x₁ x ≃lf ≃lf ≃lf) ≃lf (⋗lf x₁)
... | inj₂ x₁≤x | inj₁ x≤x₂ | _ = ⋗nd x₁ x' (≃nd x x₂ ≃lf ≃lf ≃lf) ≃lf (⋗lf x)
... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ = ⋗nd x₁ x' (≃nd x x₂ ≃lf ≃lf ≃lf) ≃lf (⋗lf x)
... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ = ⋗nd x₂ x' (≃nd x₁ x ≃lf ≃lf ≃lf) ≃lf (⋗lf x₁)
lemma-push-⋗ (⋗nd _ _ (≃nd x₁ _ ≃lf (≃nd _ _ _ _ _) ()) ≃lf (⋗lf .x₁)) _
lemma-push-⋗ (⋗nd x x' (≃nd {l₁} {r₁} {l₂} {r₂} x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) l'≃r' (⋗nd .x₁ x'₁ _ l'₁≃r'₁ l₁⋗l'₁)) (acc rs)
    with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ = ⋗nd x x' (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
... | inj₁ x≤x₁ | inj₂ x₂≤x | _ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
           let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                push-xl₁r₁≃x₂l₂r₂ = lemma-≃-push  (sym≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂)) acc-xl₂r₂ ;
                x₁l₁r₁≃push-xl₂r₂ = trans≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂) push-xl₁r₁≃x₂l₂r₂
           in ⋗nd x₂ x' x₁l₁r₁≃push-xl₂r₂ l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
... | inj₂ x₁≤x | inj₁ x≤x₂ | _ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
           let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                push-xl₁r₁≃x₂l₂r₂ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) ;
                push-xl₁r₁⋗x'₁l'₁r'₁ = lemma-push-⋗ (⋗nd x x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-xl₁r₁
           in ⋗nd x₁ x' push-xl₁r₁≃x₂l₂r₂ l'≃r' push-xl₁r₁⋗x'₁l'₁r'₁
... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
           let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                push-xl₁r₁≃x₂l₂r₂ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) ;
                push-xl₁r₁⋗x'₁l'₁r'₁ = lemma-push-⋗ (⋗nd x x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-xl₁r₁
           in ⋗nd x₁ x' push-xl₁r₁≃x₂l₂r₂ l'≃r' push-xl₁r₁⋗x'₁l'₁r'₁
... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
           let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                push-xl₁r₁≃x₂l₂r₂ = lemma-≃-push  (sym≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂)) acc-xl₂r₂ ;
                x₁l₁r₁≃push-xl₂r₂ = trans≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂) push-xl₁r₁≃x₂l₂r₂
           in ⋗nd x₂ x' x₁l₁r₁≃push-xl₂r₂ l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)

lemma-⋗-push : {t t' : PLRTree} → t ⋗ t' → (acc : Acc _≺_ t') → t ⋗ push t' acc
lemma-⋗-push (⋗lf x) _ = ⋗lf x
lemma-⋗-push (⋗nd x x' l≃r ≃lf l⋗l') _ = ⋗nd x x' l≃r ≃lf l⋗l'
lemma-⋗-push (⋗nd x x' l≃r (≃nd {l'₁} {r'₁} {l'₂} {r'₂} x'₁ x'₂  l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (⋗nd x₁ .x'₁ l₁≃r₁ _ l₁⋗l'₁)) (acc rs)
    with tot≤ x' x'₁ | tot≤ x' x'₂ | tot≤ x'₁ x'₂
... | inj₁ x'≤x'₁ | inj₁ x'≤x'₂ | _ = ⋗nd x x' l≃r (≃nd x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
... | inj₁ x'≤x'₁ | inj₂ x'₂≤x' | _ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂ =
           let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                x'₁l'₁r'₁≃push-x'l'₂r'₂ = trans≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (lemma-≃-push (sym≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂)) acc-x'l'₂r'₂)
           in ⋗nd x x'₂ l≃r x'₁l'₁r'₁≃push-x'l'₂r'₂ (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
... | inj₂ x'₁≤x' | inj₁ x'≤x'₂ | _ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
           let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                push-x'l'₁r'₁≃x'₂l'₂r'₂ = trans≃ (lemma-push-≃ (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) acc-x'l'₁r'₁) (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) ;
                x₁l₁r₁⋗push-x'l'₁r'₁ = lemma-⋗-push (⋗nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-x'l'₁r'₁
           in ⋗nd x x'₁ l≃r push-x'l'₁r'₁≃x'₂l'₂r'₂ x₁l₁r₁⋗push-x'l'₁r'₁
... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₁ x'₁≤x'₂ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
           let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                push-x'l'₁r'₁≃x'₂l'₂r'₂ = trans≃ (lemma-push-≃ (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) acc-x'l'₁r'₁) (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) ;
                x₁l₁r₁⋗push-x'l'₁r'₁ = lemma-⋗-push (⋗nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-x'l'₁r'₁
           in ⋗nd x x'₁ l≃r push-x'l'₁r'₁≃x'₂l'₂r'₂ x₁l₁r₁⋗push-x'l'₁r'₁
... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₂ x'₂≤x'₁ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂ =
           let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                x'₁l'₁r'₁≃push-x'l'₂r'₂ = trans≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (lemma-≃-push (sym≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂)) acc-x'l'₂r'₂)
           in ⋗nd x x'₂ l≃r x'₁l'₁r'₁≃push-x'l'₂r'₂ (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)

lemma-⋘-push : {t t' : PLRTree} → t ⋘ t' → (acc : Acc _≺_ t') → t ⋘ push t' acc
lemma-⋘-push (x⋘ x y z) _ = x⋘ x y z
lemma-⋘-push (l⋘ _ _ () ≃lf ≃lf) _
lemma-⋘-push (l⋘ x x' l⋘r (≃nd {l'₁} {r'₁} {l'₂} {r'₂} x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (≃nd x₂ .x'₁ l₂≃r₂ _ l₂≃l'₁)) (acc rs)
    with tot≤ x' x'₁ | tot≤ x' x'₂ | tot≤ x'₁ x'₂
... | inj₁ x'≤x'₁ | inj₁ x'≤x'₂ | _ = l⋘ x x' l⋘r (≃nd x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ l₂≃l'₁)
... | inj₁ x'≤x'₁ | inj₂ x'₂≤x' | _ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂ =
           let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                x'₁l'₁r'₁≃push-x'l'₂r'₂ = trans≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (lemma-≃-push (sym≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂)) acc-x'l'₂r'₂)
           in l⋘ x x'₂ l⋘r x'₁l'₁r'₁≃push-x'l'₂r'₂ (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ l₂≃l'₁)
... | inj₂ x'₁≤x' | inj₁ x'≤x'₂ | _ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
           let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                push-x'l'₁r'₁≃x'₂l'₂r'₂ = trans≃ (lemma-push-≃ (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) acc-x'l'₁r'₁) (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) ;
                x₂l₂r₂≃push-x'l'₁r'₁ = trans≃ (≃nd x₂ x' l₂≃r₂ l'₁≃r'₁ l₂≃l'₁) (lemma-≃-push (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) acc-x'l'₁r'₁)
           in l⋘ x x'₁ l⋘r push-x'l'₁r'₁≃x'₂l'₂r'₂ x₂l₂r₂≃push-x'l'₁r'₁
... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₁ x'₁≤x'₂ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
           let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                push-x'l'₁r'₁≃x'₂l'₂r'₂ = trans≃ (lemma-push-≃ (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) acc-x'l'₁r'₁) (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) ;
                x₂l₂r₂≃push-x'l'₁r'₁ = trans≃ (≃nd x₂ x' l₂≃r₂ l'₁≃r'₁ l₂≃l'₁) (lemma-≃-push (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) acc-x'l'₁r'₁)
           in l⋘ x x'₁ l⋘r push-x'l'₁r'₁≃x'₂l'₂r'₂ x₂l₂r₂≃push-x'l'₁r'₁
... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₂ x'₂≤x'₁ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂ =
           let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                x'₁l'₁r'₁≃push-x'l'₂r'₂ = trans≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (lemma-≃-push (sym≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂)) acc-x'l'₂r'₂)
           in l⋘ x x'₂ l⋘r x'₁l'₁r'₁≃push-x'l'₂r'₂ (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ l₂≃l'₁)
lemma-⋘-push (r⋘ x x' l⋙r ≃lf (⋗lf x₁)) _ = r⋘ x x' l⋙r ≃lf (⋗lf x₁)
lemma-⋘-push (r⋘ x x' l⋙r (≃nd {l'₁} {r'₁} {l'₂} {r'₂} x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (⋗nd x₁ .x'₁ l₁≃r₁ _ l₁⋗l'₁)) (acc rs)
    with tot≤ x' x'₁ | tot≤ x' x'₂ | tot≤ x'₁ x'₂
... | inj₁ x'≤x'₁ | inj₁ x'≤x'₂ | _ = r⋘ x x' l⋙r (≃nd x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
... | inj₁ x'≤x'₁ | inj₂ x'₂≤x' | _ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂ =
           let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                x'₁l'₁r'₁≃push-x'l'₂r'₂ = trans≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (lemma-≃-push (sym≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂)) acc-x'l'₂r'₂)
           in r⋘ x x'₂ l⋙r  x'₁l'₁r'₁≃push-x'l'₂r'₂ (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
... | inj₂ x'₁≤x' | inj₁ x'≤x'₂ | _ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
           let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                push-x'l'₁r'₁≃x'₂l'₂r'₂ = trans≃ (lemma-push-≃ (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) acc-x'l'₁r'₁) (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂)
           in r⋘ x x'₁ l⋙r push-x'l'₁r'₁≃x'₂l'₂r'₂ (lemma-⋗-push (⋗nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-x'l'₁r'₁)
... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₁ x'₁≤x'₂ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
           let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                push-x'l'₁r'₁≃x'₂l'₂r'₂ = trans≃ (lemma-push-≃ (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂)  acc-x'l'₁r'₁) (≃nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂)
           in r⋘ x x'₁ l⋙r push-x'l'₁r'₁≃x'₂l'₂r'₂ (lemma-⋗-push (⋗nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-x'l'₁r'₁)
... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₂ x'₂≤x'₁ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂ =
           let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right perfect x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                x'₁l'₁r'₁≃push-x'l'₂r'₂ = trans≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (lemma-≃-push (sym≃ (≃nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂)) acc-x'l'₂r'₂)
           in r⋘ x x'₂ l⋙r  x'₁l'₁r'₁≃push-x'l'₂r'₂ (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)

lemma-push-⋙ : {t t' : PLRTree} → t ⋙ t' → (acc : Acc _≺_ t) → push t acc ⋙ t'
lemma-push-⋙ (⋙p l⋗r) (acc rs) = ⋙p (lemma-push-⋗ l⋗r (acc rs))
lemma-push-⋙ (⋙l _ _ ≃lf _ ()) _
lemma-push-⋙ (⋙l _ _ (≃nd x₁ _ ≃lf _ _) () (⋗lf .x₁)) _
lemma-push-⋙ (⋙l x x' (≃nd {l₁} {r₁} {l₂} {r₂} x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) l'⋘r' (⋗nd .x₁ x₄ _ l₄≃r₄ l₁⋗r₄)) (acc rs)
    with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ = ⋙l x x' (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) l'⋘r' (⋗nd x₁ x₄ l₁≃r₁ l₄≃r₄ l₁⋗r₄)
... | inj₁ x≤x₁ | inj₂ x₂≤x | _ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
           let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                x₁l₁r₁≃push-xl₂r₂ = trans≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂) (lemma-≃-push  (sym≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂)) acc-xl₂r₂)
           in ⋙l x₂ x' x₁l₁r₁≃push-xl₂r₂ l'⋘r' (⋗nd x₁ x₄ l₁≃r₁ l₄≃r₄ l₁⋗r₄)
... | inj₂ x₁≤x | inj₁ x≤x₂ | _ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
           let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                push-xl₁r₁≃x₂l₂r₂ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂)
           in ⋙l x₁ x' push-xl₁r₁≃x₂l₂r₂ l'⋘r' (lemma-push-⋗ (⋗nd x x₄ l₁≃r₁ l₄≃r₄ l₁⋗r₄) acc-xl₁r₁)
... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
           let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                push-xl₁r₁≃x₂l₂r₂ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂)
           in ⋙l x₁ x' push-xl₁r₁≃x₂l₂r₂ l'⋘r' (lemma-push-⋗ (⋗nd x x₄ l₁≃r₁ l₄≃r₄ l₁⋗r₄) acc-xl₁r₁)
... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
           let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                x₁l₁r₁≃push-xl₂r₂ =  trans≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂) (lemma-≃-push  (sym≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂)) acc-xl₂r₂)
           in ⋙l x₂ x' x₁l₁r₁≃push-xl₂r₂ l'⋘r' (⋗nd x₁ x₄ l₁≃r₁ l₄≃r₄ l₁⋗r₄)
lemma-push-⋙ (⋙r _ _ ≃lf (⋙p ()) ≃lf) _
lemma-push-⋙ (⋙r x x' (≃nd {l₁} {r₁} {l₂} {r₂} x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) l'⋙r' (≃nd .x₁ x₃ _ l₃≃r₃ l₁≃l₃)) (acc rs)
    with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ = ⋙r x x' (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) l'⋙r' (≃nd x₁ x₃ l₁≃r₁ l₃≃r₃ l₁≃l₃)
... | inj₁ x≤x₁ | inj₂ x₂≤x | _ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
           let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                x₁l₁r₁≃push-xl₂r₂ = trans≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂) (lemma-≃-push (sym≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂)) acc-xl₂r₂)
           in ⋙r x₂ x' x₁l₁r₁≃push-xl₂r₂ l'⋙r' (≃nd x₁ x₃ l₁≃r₁ l₃≃r₃ l₁≃l₃)
... | inj₂ x₁≤x | inj₁ x≤x₂ | _ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
           let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                push-xl₁r₁≃x₂l₂r₂ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) ;
                push-xl₁r₁≃x₃l₃r₃ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₃ l₁≃r₁ l₃≃r₃ l₁≃l₃)
           in ⋙r x₁ x' push-xl₁r₁≃x₂l₂r₂ l'⋙r' push-xl₁r₁≃x₃l₃r₃
... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
           let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                push-xl₁r₁≃x₂l₂r₂ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) ;
                push-xl₁r₁≃x₃l₃r₃ = trans≃ (lemma-push-≃ (≃nd x x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) acc-xl₁r₁) (≃nd x x₃ l₁≃r₁ l₃≃r₃ l₁≃l₃)
           in ⋙r x₁ x' push-xl₁r₁≃x₂l₂r₂ l'⋙r' push-xl₁r₁≃x₃l₃r₃
... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
           let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                x₁l₁r₁≃push-xl₂r₂ = trans≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂) (lemma-≃-push (sym≃ (≃nd x₁ x l₁≃r₁ l₂≃r₂ l₁≃l₂)) acc-xl₂r₂)
           in ⋙r x₂ x' x₁l₁r₁≃push-xl₂r₂ l'⋙r' (≃nd x₁ x₃ l₁≃r₁ l₃≃r₃ l₁≃l₃)

mutual
  lemma-⋙r-push : {l r l' r' : PLRTree}(x x' : A) → l ≃ r → l' ⋙ r' → l ≃ l' → (acc : Acc _≺_ (node right x' l' r')) → (node perfect x l r) ⋙ push (node right x' l' r') acc
  lemma-⋙r-push x x' l≃r (⋙p (⋗lf x'₁)) (≃nd x₁ .x'₁ ≃lf ≃lf ≃lf) (acc rs)
      with tot≤ x' x'₁
  ... | inj₁ x'≤x'₁ = ⋙r x x' l≃r (⋙p (⋗lf x'₁)) (≃nd x₁ x'₁ ≃lf ≃lf ≃lf)
  ... | inj₂ x'₁≤x' = ⋙r x x'₁ l≃r (⋙p (⋗lf x')) (≃nd x₁ x' ≃lf ≃lf ≃lf)
  lemma-⋙r-push x x' l≃r (⋙p (⋗nd {l'₁} {r'₁} {l'₂} {r'₂} x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁⋗l'₂)) (≃nd x₁ .x'₁ l₁≃r₁ _ l₁≃l'₁) (acc rs)
        with tot≤ x' x'₁ | tot≤ x' x'₂ | tot≤ x'₁ x'₂
  ... | inj₁ x'≤x'₁ | inj₁ x'≤x'₂ | _ = ⋙r x x' l≃r (⋙p (⋗nd x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁⋗l'₂)) (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)
  ... | inj₁ x'≤x'₁ | inj₂ x'₂≤x' | _ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂  =
             let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right right x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋗push-x'l'₂r'₂ = lemma-⋗-push (⋗nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁⋗l'₂) acc-x'l'₂r'₂
             in ⋙r x x'₂ l≃r (⋙p x'₁l'₁r'₁⋗push-x'l'₂r'₂) (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)
  ... | inj₂ x'₁≤x' | inj₁ x'≤x'₂ | _ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left right x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋗x'₂l'₂r'₂ = lemma-push-⋗ (⋗nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁⋗l'₂) acc-x'l'₁r'₁ ;
                  x₁l₁r₁≃push-x'l'₁r'₁ = trans≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁) (lemma-≃-push (sym≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)) acc-x'l'₁r'₁)
             in ⋙r x x'₁ l≃r (⋙p push-x'l'₁r'₁⋗x'₂l'₂r'₂) x₁l₁r₁≃push-x'l'₁r'₁
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₁ x'₁≤x'₂ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left right x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋗x'₂l'₂r'₂ = lemma-push-⋗ (⋗nd x' x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁⋗l'₂) acc-x'l'₁r'₁ ;
                  x₁l₁r₁≃push-x'l'₁r'₁ = trans≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁) (lemma-≃-push (sym≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)) acc-x'l'₁r'₁)
             in ⋙r x x'₁ l≃r (⋙p push-x'l'₁r'₁⋗x'₂l'₂r'₂) x₁l₁r₁≃push-x'l'₁r'₁
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₂ x'₂≤x'₁ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂ =
             let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right right x' (node perfect x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋗push-x'l'₂r'₂ = lemma-⋗-push (⋗nd x'₁ x' l'₁≃r'₁ l'₂≃r'₂ l'₁⋗l'₂) acc-x'l'₂r'₂
             in ⋙r x x'₂ l≃r (⋙p x'₁l'₁r'₁⋗push-x'l'₂r'₂) (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)
  lemma-⋙r-push x x' l≃r (⋙l {l'₁} {r'₁} {l'₂} {r'₂} x'₁ x'₂ l'₁≃r'₁ l'₂⋘r'₂ l'₁⋗r'₂) (≃nd x₁ .x'₁ l₁≃r₁ _ l₁≃l'₁) (acc rs)
        with tot≤ x' x'₁ | tot≤ x' x'₂ | tot≤ x'₁ x'₂
  ... | inj₁ x'≤x'₁ | inj₁ x'≤x'₂ | _ = ⋙r x x' l≃r (⋙l x'₁ x'₂ l'₁≃r'₁ l'₂⋘r'₂ l'₁⋗r'₂) (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)
  ... | inj₁ x'≤x'₁ | inj₂ x'₂≤x' | _ rewrite lemma-≡-height left x' x'₂ l'₂ r'₂  =
             let acc-x'l'₂r'₂ = rs (node left x' l'₂ r'₂) (lemma-≺-right right x' (node perfect x'₁ l'₁ r'₁) (node left x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋙push-x'l'₂r'₂ = lemma-⋙l-push x'₁ x' l'₁≃r'₁ l'₂⋘r'₂ l'₁⋗r'₂ acc-x'l'₂r'₂
             in ⋙r x x'₂ l≃r  x'₁l'₁r'₁⋙push-x'l'₂r'₂ (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)
  ... | inj₂ x'₁≤x' | inj₁ x'≤x'₂ | _ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left right x' (node perfect x'₁ l'₁ r'₁) (node left x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋙x'₂l'₂r'₂ = lemma-push-⋙ (⋙l x' x'₂ l'₁≃r'₁ l'₂⋘r'₂ l'₁⋗r'₂) acc-x'l'₁r'₁ ;
                  x₁l₁r₁≃push-x'l'₁r'₁ = trans≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁) (lemma-≃-push (sym≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)) acc-x'l'₁r'₁)
             in ⋙r x x'₁ l≃r push-x'l'₁r'₁⋙x'₂l'₂r'₂ x₁l₁r₁≃push-x'l'₁r'₁
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₁ x'₁≤x'₂ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left right x' (node perfect x'₁ l'₁ r'₁) (node left x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋙x'₂l'₂r'₂ = lemma-push-⋙ (⋙l x' x'₂ l'₁≃r'₁ l'₂⋘r'₂ l'₁⋗r'₂) acc-x'l'₁r'₁ ;
                  x₁l₁r₁≃push-x'l'₁r'₁ = trans≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁) (lemma-≃-push (sym≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)) acc-x'l'₁r'₁)
             in ⋙r x x'₁ l≃r push-x'l'₁r'₁⋙x'₂l'₂r'₂ x₁l₁r₁≃push-x'l'₁r'₁
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₂ x'₂≤x'₁ rewrite lemma-≡-height left x' x'₂ l'₂ r'₂ =
             let acc-x'l'₂r'₂ = rs (node left x' l'₂ r'₂) (lemma-≺-right right x' (node perfect x'₁ l'₁ r'₁) (node left x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋙push-x'l'₂r'₂ = lemma-⋙l-push x'₁ x' l'₁≃r'₁ l'₂⋘r'₂ l'₁⋗r'₂ acc-x'l'₂r'₂
             in ⋙r x x'₂ l≃r  x'₁l'₁r'₁⋙push-x'l'₂r'₂ (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)

  lemma-⋙r-push x x' l≃r (⋙r {l'₁} {r'₁} {l'₂} {r'₂} x'₁ x'₂ l'₁≃r'₁ l'₂⋙r'₂ l'₁≃l'₂) (≃nd x₁ .x'₁ l₁≃r₁ _ l₁≃l'₁) (acc rs)
        with tot≤ x' x'₁ | tot≤ x' x'₂ | tot≤ x'₁ x'₂
  ... | inj₁ x'≤x'₁ | inj₁ x'≤x'₂ | _ = ⋙r x x' l≃r (⋙r x'₁ x'₂ l'₁≃r'₁ l'₂⋙r'₂ l'₁≃l'₂) (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)
  ... | inj₁ x'≤x'₁ | inj₂ x'₂≤x' | _ rewrite lemma-≡-height right x' x'₂ l'₂ r'₂  =
             let acc-x'l'₂r'₂ = rs (node right x' l'₂ r'₂) (lemma-≺-right right x' (node perfect x'₁ l'₁ r'₁) (node right x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋙push-x'l'₂r'₂ = lemma-⋙r-push x'₁ x' l'₁≃r'₁ l'₂⋙r'₂ l'₁≃l'₂ acc-x'l'₂r'₂
             in ⋙r x x'₂ l≃r x'₁l'₁r'₁⋙push-x'l'₂r'₂ (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)
  ... | inj₂ x'₁≤x' | inj₁ x'≤x'₂ | _ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left right x' (node perfect x'₁ l'₁ r'₁) (node right x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋙x'₂l'₂r'₂ = lemma-push-⋙ (⋙r x' x'₂ l'₁≃r'₁ l'₂⋙r'₂ l'₁≃l'₂) acc-x'l'₁r'₁ ;
                  x₁l₁r₁≃push-x'l'₁r'₁ = trans≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁) (lemma-≃-push (sym≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)) acc-x'l'₁r'₁)
             in ⋙r x x'₁ l≃r push-x'l'₁r'₁⋙x'₂l'₂r'₂ x₁l₁r₁≃push-x'l'₁r'₁
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₁ x'₁≤x'₂ rewrite lemma-≡-height perfect x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node perfect x' l'₁ r'₁) (lemma-≺-left right x' (node perfect x'₁ l'₁ r'₁) (node right x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋙x'₂l'₂r'₂ = lemma-push-⋙ (⋙r x' x'₂ l'₁≃r'₁ l'₂⋙r'₂ l'₁≃l'₂) acc-x'l'₁r'₁ ;
                  x₁l₁r₁≃push-x'l'₁r'₁ = trans≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁) (lemma-≃-push (sym≃ (≃nd x₁ x' l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)) acc-x'l'₁r'₁)
             in ⋙r x x'₁ l≃r push-x'l'₁r'₁⋙x'₂l'₂r'₂ x₁l₁r₁≃push-x'l'₁r'₁
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₂ x'₂≤x'₁ rewrite lemma-≡-height right x' x'₂ l'₂ r'₂ =
             let acc-x'l'₂r'₂ = rs (node right x' l'₂ r'₂) (lemma-≺-right right x' (node perfect x'₁ l'₁ r'₁) (node right x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋙push-x'l'₂r'₂ = lemma-⋙r-push x'₁ x' l'₁≃r'₁ l'₂⋙r'₂ l'₁≃l'₂ acc-x'l'₂r'₂
             in ⋙r x x'₂ l≃r x'₁l'₁r'₁⋙push-x'l'₂r'₂ (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)

  lemma-push-l⋘ : {l r l' r' : PLRTree}(x x' : A) → l ⋘ r → l' ≃ r' → r ≃ l' → (acc : Acc _≺_ (node left x l r)) → push (node left x l r) acc ⋘ node perfect x' l' r'
  lemma-push-l⋘ x x' (x⋘ x₁ x₂ x₃) l'≃r' (≃nd .x₃ x'₁ ≃lf ≃lf ≃lf) (acc rs)
      with tot≤ x x₁ | tot≤ x x₃ | tot≤ x₁ x₃
  ... | inj₁ x≤x₁ | inj₁ x≤x₃ | _ = l⋘ x x' (x⋘ x₁ x₂ x₃) l'≃r' (≃nd x₃ x'₁ ≃lf ≃lf ≃lf)
  ... | inj₁ x≤x₁ | inj₂ x₃≤x | _ = l⋘ x₃ x' (x⋘ x₁ x₂ x) l'≃r' (≃nd x x'₁ ≃lf ≃lf ≃lf)
  ... | inj₂ x₁≤x | inj₁ x≤x₃ | _
      with tot≤ x x₂
  ... | inj₁ x≤x₂ = l⋘ x₁ x' (x⋘ x x₂ x₃) l'≃r' (≃nd x₃ x'₁ ≃lf ≃lf ≃lf)
  ... | inj₂ x₂≤x = l⋘ x₁ x' (x⋘ x₂ x x₃) l'≃r' (≃nd x₃ x'₁ ≃lf ≃lf ≃lf)
  lemma-push-l⋘ x x' (x⋘ x₁ x₂ x₃) l'≃r' (≃nd .x₃ x'₁ ≃lf ≃lf ≃lf) (acc rs) | inj₂ x₁≤x | inj₂ x₃≤x | inj₁ x₁≤x₃
      with tot≤ x x₂
  ... | inj₁ x≤x₂ = l⋘ x₁ x' (x⋘ x x₂ x₃) l'≃r' (≃nd x₃ x'₁ ≃lf ≃lf ≃lf)
  ... | inj₂ x₂≤x = l⋘ x₁ x' (x⋘ x₂ x x₃) l'≃r' (≃nd x₃ x'₁ ≃lf ≃lf ≃lf)
  lemma-push-l⋘ x x' (x⋘ x₁ x₂ x₃) l'≃r' (≃nd .x₃ x'₁ ≃lf ≃lf ≃lf) (acc rs) | inj₂ x₁≤x | inj₂ x₃≤x | inj₂ x₃≤x₁ = l⋘ x₃ x' (x⋘ x₁ x₂ x) l'≃r' (≃nd x x'₁ ≃lf ≃lf ≃lf)
  lemma-push-l⋘ x x' (l⋘ {l₁} {r₁} {l₂} {r₂} x₁ x₂ l₁⋘r₁ l₂≃r₂ r₁≃l₂) l'≃r' (≃nd .x₂ x'₁ _ l'₁≃r'₁ r₂≃l'₁) (acc rs)
      with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
  ... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ = l⋘ x x' (l⋘ x₁ x₂ l₁⋘r₁ l₂≃r₂ r₁≃l₂) l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
  ... | inj₁ x≤x₁ | inj₂ x₂≤x | _ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right left x (node left x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  x₁l₁r₁⋘push-xl₂r₂ = lemma-⋘-push (l⋘ x₁ x l₁⋘r₁ l₂≃r₂ r₁≃l₂) acc-xl₂r₂ ;
                  push-xl₂r₂≃x'₁l'₁r'₁ = trans≃ (lemma-push-≃ (≃nd x x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁) acc-xl₂r₂) (≃nd x x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
             in l⋘ x₂ x' x₁l₁r₁⋘push-xl₂r₂ l'≃r' push-xl₂r₂≃x'₁l'₁r'₁
  ... | inj₂ x₁≤x | inj₁ x≤x₂ | _ rewrite lemma-≡-height left x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node left x l₁ r₁) (lemma-≺-left left x (node left x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁⋘x₂l₂r₂ = lemma-push-l⋘ x x₂ l₁⋘r₁ l₂≃r₂ r₁≃l₂ acc-xl₁r₁
             in l⋘ x₁ x' push-xl₁r₁⋘x₂l₂r₂ l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ rewrite lemma-≡-height left x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node left x l₁ r₁) (lemma-≺-left left x (node left x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁⋘x₂l₂r₂ = lemma-push-l⋘ x x₂ l₁⋘r₁ l₂≃r₂ r₁≃l₂ acc-xl₁r₁
             in l⋘ x₁ x' push-xl₁r₁⋘x₂l₂r₂ l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right left x (node left x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  x₁l₁r₁⋘push-xl₂r₂ = lemma-⋘-push (l⋘ x₁ x l₁⋘r₁ l₂≃r₂ r₁≃l₂) acc-xl₂r₂ ;
                  push-xl₂r₂≃x'₁l'₁r'₁ = trans≃ (lemma-push-≃ (≃nd x x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁) acc-xl₂r₂) (≃nd x x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
             in l⋘ x₂ x' x₁l₁r₁⋘push-xl₂r₂ l'≃r' push-xl₂r₂≃x'₁l'₁r'₁
  lemma-push-l⋘ x x' (r⋘ {l₁} {r₁} {l₂} {r₂} x₁ x₂ l₁⋙r₁ l₂≃r₂ l₁⋗l₂) l'≃r' (≃nd .x₂ x'₁ _ l'₁≃r'₁ r₂≃l'₁) (acc rs)
    with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
  ... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ = l⋘ x x' (r⋘ x₁ x₂ l₁⋙r₁ l₂≃r₂ l₁⋗l₂) l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
  ... | inj₁ x≤x₁ | inj₂ x₂≤x | _ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right left x (node right x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  x₁l₁r₁⋘push-xl₂r₂ = lemma-⋘-push (r⋘ x₁ x l₁⋙r₁ l₂≃r₂ l₁⋗l₂) acc-xl₂r₂ ;
                  push-xl₂r₂≃x'₁l'₁r'₁ = trans≃ (lemma-push-≃ (≃nd x x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁) acc-xl₂r₂) (≃nd x x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
             in l⋘ x₂ x' x₁l₁r₁⋘push-xl₂r₂ l'≃r' push-xl₂r₂≃x'₁l'₁r'₁
  ... | inj₂ x₁≤x | inj₁ x≤x₂ | _ rewrite lemma-≡-height right x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node right x l₁ r₁) (lemma-≺-left left x (node right x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁⋘x₂l₂r₂ = lemma-push-r⋘ x x₂ l₁⋙r₁ l₂≃r₂ l₁⋗l₂ acc-xl₁r₁
             in l⋘ x₁ x' push-xl₁r₁⋘x₂l₂r₂ l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ rewrite lemma-≡-height right x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node right x l₁ r₁) (lemma-≺-left left x (node right x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁⋘x₂l₂r₂ = lemma-push-r⋘ x x₂ l₁⋙r₁ l₂≃r₂ l₁⋗l₂ acc-xl₁r₁
             in l⋘ x₁ x' push-xl₁r₁⋘x₂l₂r₂ l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right left x (node right x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  x₁l₁r₁⋘push-xl₂r₂ = lemma-⋘-push (r⋘ x₁ x l₁⋙r₁ l₂≃r₂ l₁⋗l₂) acc-xl₂r₂ ;
                  push-xl₂r₂≃x'₁l'₁r'₁ = trans≃ (lemma-push-≃ (≃nd x x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁) acc-xl₂r₂) (≃nd x x'₁ l₂≃r₂ l'₁≃r'₁ r₂≃l'₁)
             in l⋘ x₂ x' x₁l₁r₁⋘push-xl₂r₂ l'≃r' push-xl₂r₂≃x'₁l'₁r'₁

  lemma-push-r⋘ : {l r l' r' : PLRTree}(x x' : A) → l ⋙ r → l' ≃ r' → l ⋗ l' → (acc : Acc _≺_ (node right x l r)) → push (node right x l r) acc ⋘ node perfect x' l' r'
  lemma-push-r⋘ x x' (⋙p (⋗lf x₁)) ≃lf (⋗lf .x₁) (acc rs)
      with tot≤ x x₁
  ... | inj₁ x≤x₁ = x⋘ x x₁ x'
  ... | inj₂ x₁≤x = x⋘ x₁ x x'
  lemma-push-r⋘  _ _ (⋙p (⋗lf x₁)) _ (⋗nd .x₁ _ _ _ ()) _
  lemma-push-r⋘ _ _ (⋙p (⋗nd x₁ _ _ _ ())) ≃lf (⋗lf .x₁) _
  lemma-push-r⋘ x x' (⋙p (⋗nd {l₁} {r₁} {l₂} {r₂} x₁ x₂ l₁≃r₁ l₂≃r₂ l₁⋗l₂)) l'≃r' (⋗nd .x₁ x'₁ _ l'₁≃r'₁ l₁⋗l'₁) (acc rs)
      with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
  ... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ = r⋘ x x' (⋙p (⋗nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁⋗l₂)) l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
  ... | inj₁ x≤x₁ | inj₂ x₂≤x | _ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  x₁l₁r₁⋗push-xl₂r₂ = lemma-⋗-push (⋗nd x₁ x l₁≃r₁ l₂≃r₂ l₁⋗l₂) acc-xl₂r₂
             in r⋘ x₂ x' (⋙p x₁l₁r₁⋗push-xl₂r₂) l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
  ... | inj₂ x₁≤x | inj₁ x≤x₂ | _ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁⋗x₂l₂r₂ = lemma-push-⋗ (⋗nd x x₂ l₁≃r₁ l₂≃r₂ l₁⋗l₂) acc-xl₁r₁ ;
                  push-xl₁r₁⋗x'₁l'₁r'₁ = lemma-push-⋗ (⋗nd x x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-xl₁r₁
             in r⋘ x₁ x' (⋙p push-xl₁r₁⋗x₂l₂r₂) l'≃r' push-xl₁r₁⋗x'₁l'₁r'₁
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  push-xl₁r₁⋗x₂l₂r₂ = lemma-push-⋗ (⋗nd x x₂ l₁≃r₁ l₂≃r₂ l₁⋗l₂) acc-xl₁r₁ ;
                  push-xl₁r₁⋗x'₁l'₁r'₁ = lemma-push-⋗ (⋗nd x x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-xl₁r₁
             in r⋘ x₁ x' (⋙p push-xl₁r₁⋗x₂l₂r₂) l'≃r' push-xl₁r₁⋗x'₁l'₁r'₁
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ rewrite lemma-≡-height perfect x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node perfect x l₂ r₂) (lemma-≺-right perfect x (node perfect x₁ l₁ r₁) (node perfect x₂ l₂ r₂)) ;
                  x₁l₁r₁⋗push-xl₂r₂ = lemma-⋗-push (⋗nd x₁ x l₁≃r₁ l₂≃r₂ l₁⋗l₂) acc-xl₂r₂
             in r⋘ x₂ x' (⋙p x₁l₁r₁⋗push-xl₂r₂) l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
  lemma-push-r⋘  _ _ (⋙l x₁ _ _ _ ()) _ (⋗lf .x₁) _
  lemma-push-r⋘ x x' (⋙l {l₁} {r₁} {l₂} {r₂} x₁ x₂ l₁≃r₁ l₂⋘r₂ l₁⋗r₂) l'≃r' (⋗nd .x₁ x'₁ _ l'₁≃r'₁ l₁⋗l'₁) (acc rs)
      with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
  ... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ = r⋘ x x' (⋙l x₁ x₂ l₁≃r₁ l₂⋘r₂ l₁⋗r₂) l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
  ... | inj₁ x≤x₁ | inj₂ x₂≤x | _ rewrite lemma-≡-height left x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node left x l₂ r₂) (lemma-≺-right right x (node perfect x₁ l₁ r₁) (node left x₂ l₂ r₂)) ;
                  x₁l₁r₁⋙push-xl₂r₂ = lemma-⋙l-push x₁ x l₁≃r₁ l₂⋘r₂ l₁⋗r₂ acc-xl₂r₂
             in r⋘ x₂ x' x₁l₁r₁⋙push-xl₂r₂ l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
  ... | inj₂ x₁≤x | inj₁ x≤x₂ | _ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left right x (node perfect x₁ l₁ r₁) (node left x₂ l₂ r₂)) ;
                  push-xl₁r₁⋙x₂l₂r₂ = lemma-push-⋙ (⋙l x x₂ l₁≃r₁ l₂⋘r₂ l₁⋗r₂) acc-xl₁r₁ ;
                  push-xl₁r₁⋗x'₁l'₁r'₁ = lemma-push-⋗ (⋗nd x x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-xl₁r₁
             in r⋘ x₁ x' push-xl₁r₁⋙x₂l₂r₂ l'≃r' push-xl₁r₁⋗x'₁l'₁r'₁
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left right x (node perfect x₁ l₁ r₁) (node left x₂ l₂ r₂)) ;
                  push-xl₁r₁⋙x₂l₂r₂ = lemma-push-⋙ (⋙l x x₂ l₁≃r₁ l₂⋘r₂ l₁⋗r₂) acc-xl₁r₁ ;
                  push-xl₁r₁⋗x'₁l'₁r'₁ = lemma-push-⋗ (⋗nd x x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-xl₁r₁
             in r⋘ x₁ x' push-xl₁r₁⋙x₂l₂r₂ l'≃r' push-xl₁r₁⋗x'₁l'₁r'₁
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ rewrite lemma-≡-height left x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node left x l₂ r₂) (lemma-≺-right right x (node perfect x₁ l₁ r₁) (node left x₂ l₂ r₂)) ;
                  x₁l₁r₁⋙push-xl₂r₂ = lemma-⋙l-push x₁ x l₁≃r₁ l₂⋘r₂ l₁⋗r₂ acc-xl₂r₂
             in r⋘ x₂ x' x₁l₁r₁⋙push-xl₂r₂ l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
  lemma-push-r⋘ _ _ (⋙r x₁ _ ≃lf (⋙p ()) ≃lf) ≃lf (⋗lf .x₁) _
  lemma-push-r⋘ _ _ (⋙r x₁ x₂ ≃lf (⋙l _ _ _ _ _) ()) ≃lf (⋗lf .x₁) _
  lemma-push-r⋘ _ _ (⋙r x₁ x₂ ≃lf (⋙r _ _ _ _ _) ()) ≃lf (⋗lf .x₁) _
  lemma-push-r⋘ x x' (⋙r {l₁} {r₁} {l₂} {r₂} x₁ x₂ l₁≃r₁ l₂⋙r₂ l₁≃l₂) l'≃r' (⋗nd .x₁ x'₁ _ l'₁≃r'₁ l₁⋗l'₁) (acc rs)
      with tot≤ x x₁ | tot≤ x x₂ | tot≤ x₁ x₂
  ... | inj₁ x≤x₁ | inj₁ x≤x₂ | _ = r⋘ x x' (⋙r x₁ x₂ l₁≃r₁ l₂⋙r₂ l₁≃l₂) l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
  ... | inj₁ x≤x₁ | inj₂ x₂≤x | _ rewrite lemma-≡-height right x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node right x l₂ r₂) (lemma-≺-right right x (node perfect x₁ l₁ r₁) (node right x₂ l₂ r₂)) ;
                  x₁l₁r₁⋙push-xl₂r₂ = lemma-⋙r-push x₁ x l₁≃r₁ l₂⋙r₂ l₁≃l₂ acc-xl₂r₂
             in r⋘ x₂ x' x₁l₁r₁⋙push-xl₂r₂ l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)
  ... | inj₂ x₁≤x | inj₁ x≤x₂ | _ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left right x (node perfect x₁ l₁ r₁) (node right x₂ l₂ r₂)) ;
                  push-xl₁r₁⋙x₂l₂r₂ = lemma-push-⋙ (⋙r x x₂ l₁≃r₁ l₂⋙r₂ l₁≃l₂) acc-xl₁r₁ ;
                  push-xl₁r₁⋗x'₁l'₁r'₁ = lemma-push-⋗ (⋗nd x x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-xl₁r₁
             in r⋘ x₁ x' push-xl₁r₁⋙x₂l₂r₂ l'≃r' push-xl₁r₁⋗x'₁l'₁r'₁
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₁ x₁≤x₂ rewrite lemma-≡-height perfect x x₁ l₁ r₁ =
             let acc-xl₁r₁ = rs (node perfect x l₁ r₁) (lemma-≺-left right x (node perfect x₁ l₁ r₁) (node right x₂ l₂ r₂)) ;
                  push-xl₁r₁⋙x₂l₂r₂ = lemma-push-⋙ (⋙r x x₂ l₁≃r₁ l₂⋙r₂ l₁≃l₂) acc-xl₁r₁ ;
                  push-xl₁r₁⋗x'₁l'₁r'₁ = lemma-push-⋗ (⋗nd x x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁) acc-xl₁r₁
             in r⋘ x₁ x' push-xl₁r₁⋙x₂l₂r₂ l'≃r' push-xl₁r₁⋗x'₁l'₁r'₁
  ... | inj₂ x₁≤x | inj₂ x₂≤x | inj₂ x₂≤x₁ rewrite lemma-≡-height right x x₂ l₂ r₂ =
             let acc-xl₂r₂ = rs (node right x l₂ r₂) (lemma-≺-right right x (node perfect x₁ l₁ r₁) (node right x₂ l₂ r₂)) ;
                  x₁l₁r₁⋙push-xl₂r₂ = lemma-⋙r-push x₁ x l₁≃r₁ l₂⋙r₂ l₁≃l₂ acc-xl₂r₂
             in r⋘ x₂ x' x₁l₁r₁⋙push-xl₂r₂ l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)

  lemma-⋙l-push : {l r l' r' : PLRTree}(x x' : A) → l ≃ r → l' ⋘ r' → l ⋗ r' → (acc : Acc _≺_ (node left x' l' r')) → node perfect x l r ⋙ push (node left x' l' r') acc
  lemma-⋙l-push x x' l≃r (x⋘ x'₁ x'₂ x'₃) (⋗nd x₁ .x'₃ x₂≃x₃ ≃lf (⋗lf x₂)) (acc rs)
      with tot≤ x' x'₁ | tot≤ x' x'₃ | tot≤ x'₁ x'₃
  ... | inj₁ x'≤x'₁ | inj₁ x'≤x'₃ | _ = ⋙l x x' l≃r (x⋘ x'₁ x'₂ x'₃) (⋗nd x₁ x'₃ x₂≃x₃ ≃lf (⋗lf x₂))
  ... | inj₁ x'≤x'₁ | inj₂ x'₃≤x' | _ = ⋙l x x'₃ l≃r (x⋘ x'₁ x'₂ x') (⋗nd x₁ x' x₂≃x₃ ≃lf (⋗lf x₂))
  ... | inj₂ x'₁≤x' | inj₁ x'≤x'₃ | _
      with tot≤ x' x'₂
  ... | inj₁ x'≤x'₂ = ⋙l x x'₁ l≃r (x⋘ x' x'₂ x'₃) (⋗nd x₁ x'₃ x₂≃x₃ ≃lf (⋗lf x₂))
  ... | inj₂ x'₂≤x' = ⋙l x x'₁ l≃r (x⋘ x'₂ x' x'₃) (⋗nd x₁ x'₃ x₂≃x₃ ≃lf (⋗lf x₂))
  lemma-⋙l-push x x' l≃r (x⋘ x'₁ x'₂ x'₃) (⋗nd x₁ .x'₃ x₂≃x₃ ≃lf (⋗lf x₂)) (acc rs) | inj₂ x'₁≤x' | inj₂ x'₃≤x' | inj₁ x'₁≤x'₃
      with tot≤ x' x'₂
  ... | inj₁ x'≤x'₂ = ⋙l x x'₁ l≃r (x⋘ x' x'₂ x'₃) (⋗nd x₁ x'₃ x₂≃x₃ ≃lf (⋗lf x₂))
  ... | inj₂ x'₂≤x' = ⋙l x x'₁ l≃r (x⋘ x'₂ x' x'₃) (⋗nd x₁ x'₃ x₂≃x₃ ≃lf (⋗lf x₂))
  lemma-⋙l-push x x' l≃r (x⋘ x'₁ x'₂ x'₃) (⋗nd x₁ .x'₃ x₂≃x₃ ≃lf (⋗lf x₂)) (acc rs) | inj₂ x'₁≤x' | inj₂ x'₃≤x' | inj₂ x'₃≤x'₁ =  ⋙l x x'₃ l≃r (x⋘ x'₁ x'₂ x') (⋗nd x₁ x' x₂≃x₃ ≃lf (⋗lf x₂))
  lemma-⋙l-push x x' l≃r (l⋘ {l'₁} {r'₁} {l'₂} {r'₂} x'₁ x'₂ l'₁⋘r'₁ l'₂≃r'₂ r'₁≃l'₂) (⋗nd x₁ .x'₂ l₁≃r₁ _ l₁⋗l'₂) (acc rs)
      with tot≤ x' x'₁ | tot≤ x' x'₂ | tot≤ x'₁ x'₂
  ... | inj₁ x'≤x'₁ | inj₁ x'≤x'₂ | _ = ⋙l x x' l≃r (l⋘ x'₁ x'₂ l'₁⋘r'₁ l'₂≃r'₂ r'₁≃l'₂) (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂)
  ... | inj₁ x'≤x'₁ | inj₂ x'₂≤x' | _ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂  =
             let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right left x' (node left x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋘push-x'l'₂r'₂ = lemma-⋘-push (l⋘ x'₁ x' l'₁⋘r'₁ l'₂≃r'₂ r'₁≃l'₂) acc-x'l'₂r'₂ ;
                  x₁l₁r₁⋗push-x'l'₂r'₂ = lemma-⋗-push (⋗nd x₁ x' l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂) acc-x'l'₂r'₂
             in ⋙l x x'₂ l≃r x'₁l'₁r'₁⋘push-x'l'₂r'₂ x₁l₁r₁⋗push-x'l'₂r'₂
  ... | inj₂ x'₁≤x' | inj₁ x'≤x'₂ | _ rewrite lemma-≡-height left x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node left x' l'₁ r'₁) (lemma-≺-left left x' (node left x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋘x'₂l'₂r'₂ = lemma-push-l⋘ x' x'₂ l'₁⋘r'₁ l'₂≃r'₂ r'₁≃l'₂ acc-x'l'₁r'₁
             in ⋙l x x'₁ l≃r push-x'l'₁r'₁⋘x'₂l'₂r'₂ (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂)
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₁ x'₁≤x'₂ rewrite lemma-≡-height left x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node left x' l'₁ r'₁) (lemma-≺-left left x' (node left x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋘x'₂l'₂r'₂ = lemma-push-l⋘ x' x'₂ l'₁⋘r'₁ l'₂≃r'₂ r'₁≃l'₂ acc-x'l'₁r'₁
             in ⋙l x x'₁ l≃r push-x'l'₁r'₁⋘x'₂l'₂r'₂ (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂)
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₂ x'₂≤x'₁ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂ =
             let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right left x' (node left x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋘push-x'l'₂r'₂ = lemma-⋘-push (l⋘ x'₁ x' l'₁⋘r'₁ l'₂≃r'₂ r'₁≃l'₂) acc-x'l'₂r'₂ ;
                  x₁l₁r₁⋗push-x'l'₂r'₂ = lemma-⋗-push (⋗nd x₁ x' l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂) acc-x'l'₂r'₂
             in ⋙l x x'₂ l≃r x'₁l'₁r'₁⋘push-x'l'₂r'₂ x₁l₁r₁⋗push-x'l'₂r'₂
  lemma-⋙l-push x x' l≃r (r⋘ {l'₁} {r'₁} {l'₂} {r'₂} x'₁ x'₂ l'₁⋙r'₁ l'₂≃r'₂ l'₁⋗l'₂) (⋗nd x₁ .x'₂ l₁≃r₁ _ l₁⋗l'₂) (acc rs)
      with tot≤ x' x'₁ | tot≤ x' x'₂ | tot≤ x'₁ x'₂
  ... | inj₁ x'≤x'₁ | inj₁ x'≤x'₂ | _ = ⋙l x x' l≃r (r⋘ x'₁ x'₂ l'₁⋙r'₁ l'₂≃r'₂ l'₁⋗l'₂) (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂)
  ... | inj₁ x'≤x'₁ | inj₂ x'₂≤x' | _ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂  =
             let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right left x' (node right x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋘push-x'l'₂r'₂ = lemma-⋘-push (r⋘ x'₁ x' l'₁⋙r'₁ l'₂≃r'₂ l'₁⋗l'₂) acc-x'l'₂r'₂ ;
                  x₁l₁r₁⋗push-x'l'₂r'₂ = lemma-⋗-push (⋗nd x₁ x' l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂) acc-x'l'₂r'₂
             in ⋙l x x'₂ l≃r x'₁l'₁r'₁⋘push-x'l'₂r'₂ x₁l₁r₁⋗push-x'l'₂r'₂
  ... | inj₂ x'₁≤x' | inj₁ x'≤x'₂ | _ rewrite lemma-≡-height right x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node right x' l'₁ r'₁) (lemma-≺-left left x' (node right x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋘x'₂l'₂r'₂ = lemma-push-r⋘ x' x'₂ l'₁⋙r'₁ l'₂≃r'₂ l'₁⋗l'₂ acc-x'l'₁r'₁
             in ⋙l x x'₁ l≃r push-x'l'₁r'₁⋘x'₂l'₂r'₂ (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂)
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₁ x'₁≤x'₂ rewrite lemma-≡-height right x' x'₁ l'₁ r'₁ =
             let acc-x'l'₁r'₁ = rs (node right x' l'₁ r'₁) (lemma-≺-left left x' (node right x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  push-x'l'₁r'₁⋘x'₂l'₂r'₂ = lemma-push-r⋘ x' x'₂ l'₁⋙r'₁ l'₂≃r'₂ l'₁⋗l'₂ acc-x'l'₁r'₁
             in ⋙l x x'₁ l≃r push-x'l'₁r'₁⋘x'₂l'₂r'₂ (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂)
  ... | inj₂ x'₁≤x' | inj₂ x'₂≤x' | inj₂ x'₂≤x'₁ rewrite lemma-≡-height perfect x' x'₂ l'₂ r'₂ =
             let acc-x'l'₂r'₂ = rs (node perfect x' l'₂ r'₂) (lemma-≺-right left x' (node right x'₁ l'₁ r'₁) (node perfect x'₂ l'₂ r'₂)) ;
                  x'₁l'₁r'₁⋘push-x'l'₂r'₂ = lemma-⋘-push (r⋘ x'₁ x' l'₁⋙r'₁ l'₂≃r'₂ l'₁⋗l'₂) acc-x'l'₂r'₂ ;
                  x₁l₁r₁⋗push-x'l'₂r'₂ = lemma-⋗-push (⋗nd x₁ x' l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂) acc-x'l'₂r'₂
             in ⋙l x x'₂ l≃r x'₁l'₁r'₁⋘push-x'l'₂r'₂ x₁l₁r₁⋗push-x'l'₂r'₂

lemma-⋙-push : {t t' : PLRTree} → t ⋙ t' → (acc : Acc _≺_ t') → t ⋙ push t' acc
lemma-⋙-push (⋙p l⋗r) (acc rs) = ⋙p (lemma-⋗-push l⋗r (acc rs))
lemma-⋙-push (⋙l x x' l≃r l'⋘r' l⋗r') (acc rs) = lemma-⋙l-push x x' l≃r l'⋘r' l⋗r' (acc rs)
lemma-⋙-push (⋙r x x' l≃r l'⋙r' l≃l') (acc rs) = lemma-⋙r-push x x' l≃r l'⋙r' l≃l' (acc rs)

lemma-push-⋘ : {t t' : PLRTree} → t ⋘ t' → (acc : Acc _≺_ t) → push t acc ⋘ t'
lemma-push-⋘ (x⋘ x y z) _
    with tot≤ x y
... | inj₁ x≤y = x⋘ x y z
... | inj₂ y≤x = x⋘ y x z
lemma-push-⋘ (l⋘ x x' l⋘r l'≃r' r≃l') (acc rs) = lemma-push-l⋘ x x' l⋘r l'≃r' r≃l' (acc rs)
lemma-push-⋘ (r⋘ x x' l⋙r l'≃r' l⋗l') (acc rs) = lemma-push-r⋘ x x' l⋙r l'≃r' l⋗l' (acc rs)

lemma-push-complete-≃ : {l r : PLRTree}(x : A) → Complete l → Complete r → l ≃ r → (acc : Acc _≺_ (node perfect x l r)) → Complete (push (node perfect x l r) acc)
lemma-push-complete-≃ {l} {r} x cl cr l≃r (acc rs)
    with l | r | l≃r | cl | cr
... | leaf | leaf | ≃lf | _ | _ = perfect x leaf leaf ≃lf
... | node perfect x' l' r' | node perfect x'' l'' r'' | ≃nd .x' .x'' l'≃r' l''≃r'' l'≃l'' | perfect .x' cl' cr' _ | perfect .x'' cl'' cr'' _
    with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
... | inj₁ x≤x' | inj₁ x≤x'' | _ = perfect x (perfect x' cl' cr' l'≃r') (perfect x'' cl'' cr'' l''≃r'') (≃nd x' x'' l'≃r' l''≃r'' l'≃l'')
... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height perfect x x'' l'' r'' =
           let acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                xl''r''≃push-xl''r'' = lemma-≃-push (sym≃ (≃nd x x l'≃r' l''≃r'' l'≃l'')) acc-xl''r'' ;
                x'l'r'≃push-xl''r'' = trans≃ (≃nd x' x l'≃r' l''≃r'' l'≃l'') xl''r''≃push-xl''r''
           in perfect x'' (perfect x' cl' cr' l'≃r') (lemma-push-complete-≃ x cl'' cr'' l''≃r'' acc-xl''r'') x'l'r'≃push-xl''r''
... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height perfect x x' l' r' =
           let acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                push-xl'r'≃xl'r' = lemma-push-≃ (≃nd x x l'≃r' l''≃r'' l'≃l'') acc-xl'r' ;
                push-xl'r'≃x''l''r'' = trans≃ push-xl'r'≃xl'r' (≃nd x x'' l'≃r' l''≃r'' l'≃l'')
           in perfect x' (lemma-push-complete-≃ x cl' cr' l'≃r' acc-xl'r') (perfect x'' cl'' cr'' l''≃r'') push-xl'r'≃x''l''r''
... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height perfect x x' l' r' =
           let acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                push-xl'r'≃xl'r' = lemma-push-≃ (≃nd x x l'≃r' l''≃r'' l'≃l'') acc-xl'r' ;
                push-xl'r'≃x''l''r'' = trans≃ push-xl'r'≃xl'r' (≃nd x x'' l'≃r' l''≃r'' l'≃l'')
           in perfect x' (lemma-push-complete-≃ x cl' cr' l'≃r' acc-xl'r') (perfect x'' cl'' cr'' l''≃r'') push-xl'r'≃x''l''r''
... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height perfect x x'' l'' r'' =
           let acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                xl''r''≃push-xl''r'' = lemma-≃-push (sym≃ (≃nd x x l'≃r' l''≃r'' l'≃l'')) acc-xl''r'' ;
                x'l'r'≃push-xl''r'' = trans≃ (≃nd x' x l'≃r' l''≃r'' l'≃l'') xl''r''≃push-xl''r''
           in perfect x'' (perfect x' cl' cr' l'≃r') (lemma-push-complete-≃ x cl'' cr'' l''≃r'' acc-xl''r'') x'l'r'≃push-xl''r''

lemma-push-complete-⋗ : {l r : PLRTree}(x : A) → Complete l → Complete r → l ⋗ r → (acc : Acc _≺_ (node right x l r)) → Complete (push (node right x l r) acc)
lemma-push-complete-⋗ {l} {r} x cl cr l⋗r (acc rs)
    with l | r | l⋗r | cl | cr
... | leaf | _ | () | _ | _
... | node perfect x' leaf leaf | leaf | ⋗lf .x' | perfect .x' leaf leaf ≃lf | leaf
    with tot≤ x x'
... | inj₁ x≤x' = right x (perfect x' leaf leaf ≃lf) leaf (⋙p (⋗lf x'))
... | inj₂ x'≤x = right x' (perfect x leaf leaf ≃lf) leaf (⋙p (⋗lf x))
lemma-push-complete-⋗ x cl cr l⋗r (acc rs) | node perfect x' l' r' | node perfect x'' l'' r'' | ⋗nd .x' .x'' l'≃r' l''≃r'' l'⋗l'' | perfect .x' cl' cr' _ | perfect .x'' cl'' cr'' _
    with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
... | inj₁ x≤x' | inj₁ x≤x'' | _ = right x (perfect x' cl' cr' l'≃r') (perfect x'' cl'' cr'' l''≃r'') (⋙p (⋗nd x' x'' l'≃r' l''≃r'' l'⋗l''))
... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height perfect x x'' l'' r'' =
           let acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right right x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                x'l'r'⋗push-xl''r'' = lemma-⋗-push (⋗nd x' x l'≃r' l''≃r'' l'⋗l'') acc-xl''r''
           in right x'' (perfect x' cl' cr' l'≃r') (lemma-push-complete-≃ x cl'' cr'' l''≃r'' acc-xl''r'') (⋙p x'l'r'⋗push-xl''r'')
... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height perfect x x' l' r' =
           let acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left right x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                push-xl'r'⋗x''l''r'' = lemma-push-⋗ (⋗nd x x'' l'≃r' l''≃r'' l'⋗l'') acc-xl'r'
           in right x' (lemma-push-complete-≃ x cl' cr' l'≃r' acc-xl'r') (perfect x'' cl'' cr'' l''≃r'') (⋙p push-xl'r'⋗x''l''r'')
... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height perfect x x' l' r' =
           let acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left right x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                push-xl'r'⋗x''l''r'' = lemma-push-⋗ (⋗nd x x'' l'≃r' l''≃r'' l'⋗l'') acc-xl'r'
           in right x' (lemma-push-complete-≃ x cl' cr' l'≃r' acc-xl'r') (perfect x'' cl'' cr'' l''≃r'') (⋙p push-xl'r'⋗x''l''r'')
... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height perfect x x'' l'' r'' =
           let acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right right x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                x'l'r'⋗push-xl''r'' = lemma-⋗-push (⋗nd x' x l'≃r' l''≃r'' l'⋗l'') acc-xl''r''
           in right x'' (perfect x' cl' cr' l'≃r') (lemma-push-complete-≃ x cl'' cr'' l''≃r'' acc-xl''r'') (⋙p x'l'r'⋗push-xl''r'')

mutual
  lemma-push-complete-⋙ : {l r : PLRTree}(x : A) → Complete l → Complete r → l ⋙ r → (acc : Acc _≺_ (node right x l r)) → Complete (push (node right x l r) acc)
  lemma-push-complete-⋙ {l} {r} x cl cr l⋙r (acc rs)
      with l | r | l⋙r | cl | cr
  ... | leaf | _ | ⋙p () | _ | _
  ... | node perfect x' leaf leaf | leaf | ⋙p (⋗lf .x') | perfect .x' leaf leaf ≃lf | leaf =
             lemma-push-complete-⋗ x (perfect x' leaf leaf ≃lf) leaf (⋗lf x') (acc rs)
  ... | node perfect x' l' r' | node perfect x'' l'' r'' | ⋙p (⋗nd .x' .x'' l'≃r' l''≃r'' l'⋗l'') | perfect .x' cl' cr' _ | perfect .x'' cl'' cr'' _ =
             lemma-push-complete-⋗ x (perfect x' cl' cr' l'≃r') (perfect x'' cl'' cr'' l''≃r'') (⋗nd x' x'' l'≃r' l''≃r'' l'⋗l'') (acc rs)
  ... | node perfect x' leaf leaf | node left _ _ _ | ⋙p () | _ | _
  ... | node perfect x' leaf leaf | node right _ _ _ | ⋙p () | _ | _
  ... | node perfect x' l' r' | node left x'' l'' r'' | ⋙l .x' .x'' l'≃r' l''⋘r'' l'⋗r'' | perfect .x' cl' cr' _ | left .x'' cl'' cr'' _
      with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
  ... | inj₁ x≤x' | inj₁ x≤x'' | _ = right x (perfect x' cl' cr' l'≃r') (left x'' cl'' cr'' l''⋘r'') (⋙l x' x'' l'≃r' l''⋘r'' l'⋗r'')
  ... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height left x x'' l'' r'' =
             let acc-xl''r'' = rs (node left x l'' r'') (lemma-≺-right right x (node perfect x' l' r') (node left x'' l'' r'')) ;
                  x'l'r'⋙push-xl''r'' = lemma-⋙-push (⋙l x' x l'≃r' l''⋘r'' l'⋗r'') acc-xl''r''
             in right x'' (perfect x' cl' cr' l'≃r') (lemma-push-complete-⋘ x cl'' cr'' l''⋘r'' acc-xl''r'') x'l'r'⋙push-xl''r''
  ... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height perfect x x' l' r' =
             let acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left right x (node perfect x' l' r') (node left x'' l'' r'')) ;
                  push-xl'r'⋙x''l''r'' = lemma-push-⋙ (⋙l x x'' l'≃r' l''⋘r'' l'⋗r'') acc-xl'r'
             in right x' (lemma-push-complete-≃ x cl' cr' l'≃r' acc-xl'r') (left x'' cl'' cr'' l''⋘r'') push-xl'r'⋙x''l''r''
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height perfect x x' l' r' =
             let acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left right x (node perfect x' l' r') (node left x'' l'' r'')) ;
                  push-xl'r'⋙x''l''r'' = lemma-push-⋙ (⋙l x x'' l'≃r' l''⋘r'' l'⋗r'') acc-xl'r'
             in right x' (lemma-push-complete-≃ x cl' cr' l'≃r' acc-xl'r') (left x'' cl'' cr'' l''⋘r'') push-xl'r'⋙x''l''r''
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height left x x'' l'' r'' =
             let acc-xl''r'' = rs (node left x l'' r'') (lemma-≺-right right x (node perfect x' l' r') (node left x'' l'' r'')) ;
                  x'l'r'⋙push-xl''r'' = lemma-⋙-push (⋙l x' x l'≃r' l''⋘r'' l'⋗r'') acc-xl''r''
             in right x'' (perfect x' cl' cr' l'≃r') (lemma-push-complete-⋘ x cl'' cr'' l''⋘r'' acc-xl''r'') x'l'r'⋙push-xl''r''
  lemma-push-complete-⋙ x cl cr l⋙r (acc rs)| node perfect x' l' r' | node right x'' l'' r'' | ⋙r .x' .x'' l'≃r' l''⋙r'' l'≃l'' | perfect .x' cl' cr' _ | right .x'' cl'' cr'' _
      with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
  ... | inj₁ x≤x' | inj₁ x≤x'' | _ = right x (perfect x' cl' cr' l'≃r') (right x'' cl'' cr'' l''⋙r'') (⋙r x' x'' l'≃r' l''⋙r'' l'≃l'')
  ... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height right x x'' l'' r'' =
             let acc-xl''r'' = rs (node right x l'' r'') (lemma-≺-right right x (node perfect x' l' r') (node right x'' l'' r'')) ;
                  x'l'r'⋙push-xl''r'' = lemma-⋙-push (⋙r x' x l'≃r' l''⋙r'' l'≃l'') acc-xl''r''
             in right x'' (perfect x' cl' cr' l'≃r') (lemma-push-complete-⋙ x cl'' cr'' l''⋙r'' acc-xl''r'') x'l'r'⋙push-xl''r''
  ... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height perfect x x' l' r' =
             let acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left right x (node perfect x' l' r') (node right x'' l'' r'')) ;
                  push-xl'r'⋙x''l''r'' = lemma-push-⋙ (⋙r x x'' l'≃r' l''⋙r'' l'≃l'') acc-xl'r'
             in right x' (lemma-push-complete-≃ x cl' cr' l'≃r' acc-xl'r') (right x'' cl'' cr'' l''⋙r'') push-xl'r'⋙x''l''r''
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height perfect x x' l' r' =
             let acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left right x (node perfect x' l' r') (node right x'' l'' r'')) ;
                  push-xl'r'⋙x''l''r'' = lemma-push-⋙ (⋙r x x'' l'≃r' l''⋙r'' l'≃l'') acc-xl'r'
             in right x' (lemma-push-complete-≃ x cl' cr' l'≃r' acc-xl'r') (right x'' cl'' cr'' l''⋙r'') push-xl'r'⋙x''l''r''
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height right x x'' l'' r'' =
             let acc-xl''r'' = rs (node right x l'' r'') (lemma-≺-right right x (node perfect x' l' r') (node right x'' l'' r'')) ;
                  x'l'r'⋙push-xl''r'' = lemma-⋙-push (⋙r x' x l'≃r' l''⋙r'' l'≃l'') acc-xl''r''
             in right x'' (perfect x' cl' cr' l'≃r') (lemma-push-complete-⋙ x cl'' cr'' l''⋙r'' acc-xl''r'') x'l'r'⋙push-xl''r''
  lemma-push-complete-⋙ x cl cr l⋙r (acc rs) | node left _ _ _ | _ | ⋙p () | _ | _
  lemma-push-complete-⋙ x cl cr l⋙r (acc rs) | node right _ _ _ | _ | ⋙p () | _ | _

  lemma-push-complete-⋘ : {l r : PLRTree}(x : A) → Complete l → Complete r → l ⋘ r → (acc : Acc _≺_ (node left x l r)) → Complete (push (node left x l r) acc)
  lemma-push-complete-⋘ {l} {r} x cl cr l⋘r (acc rs)
      with l | r | l⋘r | cl | cr
  ... | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | left .x' cl' cr' _ | perfect .x'' cl'' cr'' _
      with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
  ... | inj₁ x≤x' | inj₁ x≤x'' | _ = left x (left x' cl' cr' l'⋘r') (perfect x'' cl'' cr'' l''≃r'') (l⋘ x' x'' l'⋘r' l''≃r'' r'≃l'')
  ... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height perfect x x'' l'' r'' =
             let acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right left x (node left x' l' r') (node perfect x'' l'' r'')) ;
                  xl''r''≃push-xl''r'' = lemma-≃-push  (≃nd x x l''≃r'' l''≃r'' (lemma-≃-≃ l''≃r'')) acc-xl''r'' ;
                  x''l''r''≃push-xl''r'' = trans≃ (≃nd x'' x l''≃r'' l''≃r'' (lemma-≃-≃ l''≃r'')) xl''r''≃push-xl''r'' ;
                  x'l'r'⋘push-xl''r'' = lemma-⋘-push (l⋘ x' x l'⋘r' l''≃r'' r'≃l'') acc-xl''r''
             in left x'' (left x' cl' cr' l'⋘r') (lemma-push-complete-≃ x cl'' cr'' l''≃r'' acc-xl''r'') x'l'r'⋘push-xl''r''
  ... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height left x x' l' r' =
             let acc-xl'r' = rs (node left x l' r') (lemma-≺-left left x (node left x' l' r') (node perfect x'' l'' r'')) ;
                  push-xl'r'⋘x''l''r'' = lemma-push-⋘ (l⋘ x x'' l'⋘r' l''≃r'' r'≃l'') acc-xl'r'
             in left x' (lemma-push-complete-⋘ x cl' cr' l'⋘r' acc-xl'r') (perfect x'' cl'' cr'' l''≃r'') push-xl'r'⋘x''l''r''
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height left x x' l' r' =
             let acc-xl'r' = rs (node left x l' r') (lemma-≺-left left x (node left x' l' r') (node perfect x'' l'' r'')) ;
                  push-xl'r'⋘x''l''r'' = lemma-push-⋘ (l⋘ x x'' l'⋘r' l''≃r'' r'≃l'') acc-xl'r'
             in left x' (lemma-push-complete-⋘ x cl' cr' l'⋘r' acc-xl'r') (perfect x'' cl'' cr'' l''≃r'') push-xl'r'⋘x''l''r''
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height perfect x x'' l'' r'' =
             let acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right left x (node left x' l' r') (node perfect x'' l'' r'')) ;
                  xl''r''≃push-xl''r'' = lemma-≃-push  (≃nd x x l''≃r'' l''≃r'' (lemma-≃-≃ l''≃r'')) acc-xl''r'' ;
                  x''l''r''≃push-xl''r'' = trans≃ (≃nd x'' x l''≃r'' l''≃r'' (lemma-≃-≃ l''≃r'')) xl''r''≃push-xl''r'' ;
                  x'l'r'⋘push-xl''r'' = lemma-⋘-push (l⋘ x' x l'⋘r' l''≃r'' r'≃l'') acc-xl''r''
             in left x'' (left x' cl' cr' l'⋘r') (lemma-push-complete-≃ x cl'' cr'' l''≃r'' acc-xl''r'') x'l'r'⋘push-xl''r''
  lemma-push-complete-⋘ x cl cr l⋘r (acc rs) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | right .x' (perfect .x'' leaf leaf ≃lf) leaf (⋙p (⋗lf .x'')) | perfect .x''' leaf leaf ≃lf
      with tot≤ x x' | tot≤ x x''' | tot≤ x' x'''
  ... | inj₁ x≤x' | inj₁ x≤x''' | _ = left x (right x' (perfect x'' leaf leaf ≃lf) leaf (⋙p (⋗lf x''))) (perfect x''' leaf leaf ≃lf) (x⋘ x' x'' x''')
  ... | inj₁ x≤x' | inj₂ x'''≤x | _ = left x''' (right x' (perfect x'' leaf leaf ≃lf) leaf (⋙p (⋗lf x''))) (perfect x leaf leaf ≃lf) (x⋘ x' x'' x)
  ... | inj₂ x'≤x | inj₁ x≤x''' | _ =
             let acc-xx'' = rs (node right x (node perfect x'' leaf leaf) leaf) (lemma-≺-left left x (node right x' (node perfect x'' leaf leaf) leaf) (node perfect x''' leaf leaf)) ;
                  cdl = lemma-push-complete-⋙ x (perfect x'' leaf leaf ≃lf) leaf (⋙p (⋗lf x'')) acc-xx''
             in left x' cdl (perfect x''' leaf leaf ≃lf) (lemma-push-⋘ (x⋘ x x'' x''') acc-xx'')
  ... | inj₂ x'≤x | inj₂ x'''≤x | inj₁ x'≤x''' =
             let acc-xx'' = rs (node right x (node perfect x'' leaf leaf) leaf) (lemma-≺-left left x (node right x' (node perfect x'' leaf leaf) leaf) (node perfect x''' leaf leaf)) ;
                  cdl = lemma-push-complete-⋙ x (perfect x'' leaf leaf ≃lf) leaf (⋙p (⋗lf x'')) acc-xx''
             in left x' cdl (perfect x''' leaf leaf ≃lf) (lemma-push-⋘ (x⋘ x x'' x''') acc-xx'')
  ... | inj₂ x'≤x | inj₂ x'''≤x | inj₂ x'''≤x' = left x''' (right x' (perfect x'' leaf leaf ≃lf) leaf (⋙p (⋗lf x''))) (perfect x leaf leaf ≃lf) (x⋘ x' x'' x)
  lemma-push-complete-⋘ x cl cr l⋘r (acc rs) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l'⋙r' l''≃r'' l'⋗l'' | right .x' cl' cr' _ | perfect .x'' cl'' cr'' _
      with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
  ... | inj₁ x≤x' | inj₁ x≤x'' | _ = left x (right x' cl' cr' l'⋙r') (perfect x'' cl'' cr'' l''≃r'') (r⋘ x' x'' l'⋙r' l''≃r'' l'⋗l'')
  ... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height perfect x x'' l'' r'' =
             let acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right left x (node right x' l' r') (node perfect x'' l'' r'')) ;
                  x'lr'⋘push-xl''r'' = lemma-⋘-push (r⋘ x' x l'⋙r' l''≃r'' l'⋗l'') acc-xl''r''
             in left x'' (right x' cl' cr' l'⋙r') (lemma-push-complete-≃ x cl'' cr'' l''≃r'' acc-xl''r'') x'lr'⋘push-xl''r''
  ... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height right x x' l' r' =
             let acc-xl'r' = rs (node right x l' r') (lemma-≺-left left x (node right x' l' r') (node perfect x'' l'' r'')) ;
                  push-xl'r'⋘x''l''r'' = lemma-push-⋘ (r⋘ x x'' l'⋙r' l''≃r'' l'⋗l'') acc-xl'r'
             in left x' (lemma-push-complete-⋙ x cl' cr' l'⋙r' acc-xl'r') (perfect x'' cl'' cr'' l''≃r'') push-xl'r'⋘x''l''r''
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height right x x' l' r' =
             let acc-xl'r' = rs (node right x l' r') (lemma-≺-left left x (node right x' l' r') (node perfect x'' l'' r'')) ;
                  push-xl'r'⋘x''l''r'' = lemma-push-⋘ (r⋘ x x'' l'⋙r' l''≃r'' l'⋗l'') acc-xl'r'
             in left x' (lemma-push-complete-⋙ x cl' cr' l'⋙r' acc-xl'r') (perfect x'' cl'' cr'' l''≃r'') push-xl'r'⋘x''l''r''
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height perfect x x'' l'' r'' =
             let acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right left x (node right x' l' r') (node perfect x'' l'' r'')) ;
                   x'lr'⋘push-xl''r'' = lemma-⋘-push (r⋘ x' x l'⋙r' l''≃r'' l'⋗l'') acc-xl''r''
             in left x'' (right x' cl' cr' l'⋙r') (lemma-push-complete-≃ x cl'' cr'' l''≃r'' acc-xl''r'') x'lr'⋘push-xl''r''

lemma-push-complete : {t : PLRTree} → Complete t → (acc : Acc _≺_ t) → Complete (push t acc)
lemma-push-complete leaf _ = leaf
lemma-push-complete (perfect {l} {r}x cl cr l≃r) (acc rs) = lemma-push-complete-≃ x cl cr l≃r (acc rs)
lemma-push-complete (left {l} {r}x cl cr l⋘r) (acc rs) = lemma-push-complete-⋘ x cl cr l⋘r (acc rs)
lemma-push-complete (right {l} {r}x cl cr l⋙r) (acc rs) = lemma-push-complete-⋙ x cl cr l⋙r (acc rs)


text:
{-# OPTIONS --experimental-irrelevance #-}
module ShapeIrrelevantIndexNoBecauseOfRecursion where

data ⊥ : Set where

record ⊤ : Set where
  constructor trivial

data Bool : Set where
  true false : Bool

True : Bool → Set
True false = ⊥
True true  = ⊤

data D : ..(b : Bool) → Set where
  c : {b : Bool} → True b → D b
-- because  of the irrelevant index,
-- D is in essence an existental type D : Set
-- with constructor c : {b : Bool} → True b → D

fromD : {b : Bool} → D b → True b
fromD (c p) = p -- should fail

cast : .(a b : Bool) → D a → D b
cast _ _ x = x

bot : ⊥
bot = fromD (cast true false (c trivial))

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Monoidal.Structure
  using (BraidedMonoidalCategory)

module Categories.Functor.Monoidal.Braided {o o′ ℓ ℓ′ e e′}
  (C : BraidedMonoidalCategory o ℓ e) (D : BraidedMonoidalCategory o′ ℓ′ e′)
  where

open import Level
open import Data.Product using (_,_)

open import Categories.Category using (module Commutation)
open import Categories.Functor using (Functor)
open import Categories.Functor.Monoidal
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism)

open NaturalIsomorphism

private
  module C = BraidedMonoidalCategory C
  module D = BraidedMonoidalCategory D

module Lax where

  -- Lax braided monoidal functors.

  record IsBraidedMonoidalFunctor (F : Functor C.U D.U)
         : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
    open Functor F

    field
      isMonoidal : IsMonoidalFunctor C.monoidalCategory D.monoidalCategory F

    open IsMonoidalFunctor isMonoidal public
    open D
    open Commutation D.U

    -- coherence condition

    field
      braiding-compat : ∀ {X Y} →
                        [ F₀ X ⊗₀ F₀ Y                  ⇒ F₀ (Y C.⊗₀ X) ]⟨
                          ⊗-homo.η (X , Y)              ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
                          F₁ (C.braiding.⇒.η (X , Y))
                        ≈ D.braiding.⇒.η (F₀ X , F₀ Y)  ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
                          ⊗-homo.η (Y , X)
                        ⟩

  record BraidedMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      F                   : Functor C.U D.U
      isBraidedMonoidal : IsBraidedMonoidalFunctor F

    open Functor F public
    open IsBraidedMonoidalFunctor isBraidedMonoidal public

    monoidalFunctor : MonoidalFunctor C.monoidalCategory D.monoidalCategory
    monoidalFunctor = record { isMonoidal = isMonoidal }

module Strong where

  -- Strong braided monoidal functors.

  record IsBraidedMonoidalFunctor (F : Functor C.U D.U)
         : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
    open Functor F

    field
      isStrongMonoidal : IsStrongMonoidalFunctor C.monoidalCategory
                                                 D.monoidalCategory F

    open IsStrongMonoidalFunctor isStrongMonoidal public
    open D
    open Commutation D.U

    -- coherence condition

    field
      braiding-compat : ∀ {X Y} →
                        [ F₀ X ⊗₀ F₀ Y                  ⇒ F₀ (Y C.⊗₀ X) ]⟨
                          ⊗-homo.⇒.η (X , Y)            ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
                          F₁ (C.braiding.⇒.η (X , Y))
                        ≈ D.braiding.⇒.η (F₀ X , F₀ Y)  ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
                          ⊗-homo.⇒.η (Y , X)
                        ⟩

    isLaxBraidedMonoidal : Lax.IsBraidedMonoidalFunctor F
    isLaxBraidedMonoidal = record
      { isMonoidal      = isMonoidal
      ; braiding-compat = braiding-compat
      }

  record BraidedMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      F                   : Functor C.U D.U
      isBraidedMonoidal : IsBraidedMonoidalFunctor F

    open Functor F public
    open IsBraidedMonoidalFunctor isBraidedMonoidal public

    monoidalFunctor : StrongMonoidalFunctor C.monoidalCategory
                                            D.monoidalCategory
    monoidalFunctor = record { isStrongMonoidal = isStrongMonoidal }

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: TOTBWF/agda-categories

max_forks_repo_name: TOTBWF/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The reflexive transitive closures of McBride, Norell and Jansson
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Construct.Closure.ReflexiveTransitive module directly
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Star where

open import Relation.Binary.Construct.Closure.ReflexiveTransitive public


text:
{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.types.Truncation
open import lib.types.TwoSemiCategory
open import lib.two-semi-categories.Functor
open import lib.two-semi-categories.FunctorInverse
open import lib.two-semi-categories.GroupToCategory

module lib.two-semi-categories.FundamentalCategory where

module _ {i} (A : Type i) where

  2-type-fundamental-cat : {{_ : has-level 2 A}} → TwoSemiCategory i i
  2-type-fundamental-cat =
    record
    { El = A
    ; Arr = _==_
    ; Arr-level = λ _ _ → ⟨⟩
    ; two-semi-cat-struct = record
      { comp = _∙_
      ; assoc = ∙-assoc
      ; pentagon-identity = ∙-assoc-pentagon
      }
    }

  =ₜ-fundamental-cat : TwoSemiCategory i i
  =ₜ-fundamental-cat =
    record
    { El = Trunc 2 A
    ; Arr = _=ₜ_
    ; Arr-level = =ₜ-level
    ; two-semi-cat-struct = record
      { comp = λ {ta} → _∙ₜ_ {ta = ta}
      ; assoc = λ {ta} → ∙ₜ-assoc {ta = ta}
      ; pentagon-identity = λ {ta} → ∙ₜ-assoc-pentagon {ta = ta}
      }
    }

module _ {i} (A : Type i) where

  2-type-to-=ₜ-fundamental-cat :
    TwoSemiFunctor (2-type-fundamental-cat (Trunc 2 A))
                   (=ₜ-fundamental-cat A)
  2-type-to-=ₜ-fundamental-cat =
    record
    { F₀ = idf (Trunc 2 A)
    ; F₁ = λ {ta} {tb} → –> (=ₜ-equiv ta tb)
    ; pres-comp = –>-=ₜ-equiv-pres-∙
      -- TODO: The following line takes a really long time to check.
      -- Can we optimize this somehow?
    ; pres-comp-coh = λ {ta} → –>-=ₜ-equiv-pres-∙-coh {ta = ta}
    }

  private
    module FunctorInv =
      FunctorInverse 2-type-to-=ₜ-fundamental-cat
                     (idf-is-equiv (Trunc 2 A))
                     (λ ta tb → snd (=ₜ-equiv ta tb))
    module InvFunctor = TwoSemiFunctor FunctorInv.functor

  =ₜ-to-2-type-fundamental-cat :
    TwoSemiFunctor (=ₜ-fundamental-cat A)
                   (2-type-fundamental-cat (Trunc 2 A))
  =ₜ-to-2-type-fundamental-cat =
    record
    { F₀ = idf (Trunc 2 A)
    ; F₁ = λ {ta} {tb} → <– (=ₜ-equiv ta tb)
    ; pres-comp = InvFunctor.pres-comp
    ; pres-comp-coh = InvFunctor.pres-comp-coh
    }

  module =ₜ-to-2-type-fundamental-cat = TwoSemiFunctor =ₜ-to-2-type-fundamental-cat

  =ₜ-to-2-type-fundamental-cat-pres-comp-β : {a b c : A}
    (p : a == b) (q : b == c)
    → =ₜ-to-2-type-fundamental-cat.pres-comp {x = [ a ]} {y = [ b ]} {z = [ c ]} [ p ]₁ [ q ]₁
      == ap-∙ [_] p q
  =ₜ-to-2-type-fundamental-cat-pres-comp-β {a} p@idp q@idp =
    =ₛ-out (FunctorInv.pres-comp-β {[ a ]} {[ a ]} {[ a ]} [ idp ]₁ [ idp ]₁)

module _ {i} (C : Type i) (c₀ : C) {{C-level : has-level 1 C}} where

  open import lib.groups.LoopSpace

  fundamental-group-to-fundamental-groupoid :
    TwoSemiFunctor (group-to-cat (Ω^S-group 0 ⊙[ C , c₀ ]))
                   (2-type-fundamental-cat C {{raise-level 1 C-level}})
  fundamental-group-to-fundamental-groupoid =
    record
    { F₀ = λ _ → c₀
    ; F₁ = λ p → p
    ; pres-comp = λ p q → idp
    ; pres-comp-coh =
        λ p q r → =ₛ-in $
          prop-path (has-level-apply (has-level-apply C-level _ _) _ _) _ _
    }

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module Basic.SmallStep where

import Data.Bool as Bool using (not)
open import Data.Bool hiding (not; if_then_else_)
open import Data.Empty
open import Data.Fin using (Fin; suc; zero; #_)
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Vec
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Unit hiding (_≤?_)
open import Data.Product
open import Data.Maybe
import Level as L

open import Basic.AST
open import Utils.Decidable
open import Utils.NatOrdLemmas

{-
Small-step semantics for While; see chapter 2.2 of the book.

The book uses the notational convenience of omitting the state on the right hand side
of the transition if there is no such state. We must define the same shorthand explicitly.

Since the book seems to do it, I also decided to index derivation sequences by their length.
This means also more cases for notatitonal shorthands. Otherwise, the definitions follow the book
faithfully.

Here I omit some commentary, since most of the things follow the same pattern as with big-step
semantics. However, I also include some lemmas specific to small-step semantics, which are
also included in the book.
-}

infixr 5 _∷_
mutual

  -- Notational shorthands for derivation sequences:

  -- Sequences with specified number of steps:
  ⟨_,_⟩_⟶_ : ∀ {n} → St n → State n → ℕ → State n → Set
  ⟨_,_⟩_⟶_ S s k s' = ⟨ S , s ⟩ k ⟶[ nothing , s' ]

  ⟨_,_⟩_⟶⟨_,_⟩ : ∀ {n} → St n → State n → ℕ → St n → State n → Set
  ⟨_,_⟩_⟶⟨_,_⟩ S s k S' s' = ⟨ S , s ⟩ k ⟶[ just S' , s' ]

  -- Sequences with unspecified number of steps:
  ⟨_,_⟩⟶*⟨_,_⟩ : ∀ {n} → St n → State n → St n → State n → Set
  ⟨_,_⟩⟶*⟨_,_⟩ S s S' s' = ∃ λ n → ⟨ S , s ⟩ n ⟶[ just S' , s' ]

  ⟨_,_⟩⟶*_ : ∀ {n} → St n → State n → State n → Set
  ⟨_,_⟩⟶*_ S s s' = ∃ λ n → ⟨ S , s ⟩ n ⟶[ nothing , s' ]

  -- Single-step transitions:
  ⟨_,_⟩⟶_ : ∀ {n} → St n → State n → State n → Set
  ⟨_,_⟩⟶_ S s s' = ⟨ S , s ⟩⟶[ nothing , s' ]

  ⟨_,_⟩⟶⟨_,_⟩ : ∀ {n} → St n → State n → St n → State n → Set
  ⟨_,_⟩⟶⟨_,_⟩ S s S' s' = ⟨ S , s ⟩⟶[ just S' , s' ]

  data ⟨_,_⟩⟶[_,_] {n : ℕ} : St n → State n → Maybe (St n) → State n → Set where

    ass :
                    ∀ {x a s}
      → --------------------------------------
        ⟨ x := a , s ⟩⟶ ( s [ x ]≔ ⟦ a ⟧ᵉ s )

    skip :
             ∀ {s}
      → ----------------
        ⟨ skip , s ⟩⟶ s

    _◄ :
                 ∀ {s s' S₁ S₂ S₁'} →
              ⟨ S₁ , s ⟩⟶⟨ S₁' , s' ⟩
      → --------------------------------------
        ⟨ (S₁ , S₂) , s ⟩⟶⟨ (S₁' , S₂) , s' ⟩

    _∙ :
              ∀ {s s' S₁ S₂} →
               ⟨ S₁ , s ⟩⟶ s'
      → ------------------------------
        ⟨ (S₁ , S₂) , s ⟩⟶⟨ S₂ , s' ⟩

    if-true :
             ∀ {b s S₁ S₂}  →  T (⟦ b ⟧ᵉ s)
      → ---------------------------------------
        ⟨ if b then S₁ else S₂ , s ⟩⟶⟨ S₁ , s ⟩

    if-false :
             ∀ {b s S₁ S₂}  →  F (⟦ b ⟧ᵉ s)
      → ---------------------------------------
        ⟨ if b then S₁ else S₂ , s ⟩⟶⟨ S₂ , s ⟩

    while :
                                   ∀ {b s S}
      → ----------------------------------------------------------------------
        ⟨ while b do S , s ⟩⟶⟨ (if b then (S , while b do S) else skip) , s ⟩

  -- Derivation sequences
  data ⟨_,_⟩_⟶[_,_] {n : ℕ} : St n → State n → ℕ → Maybe (St n) → State n → Set where

    pause  :
               ∀ {s S}
      → -----------------------
        ⟨ S , s ⟩ 0 ⟶⟨ S , s ⟩

    _stop :
          ∀ {s s' S} →
         ⟨ S , s ⟩⟶ s'
      → -----------------
        ⟨ S , s ⟩ 1 ⟶ s'

    _∷_ :
                       ∀ {k s₁ s₂ s₃ S₁ S₂ S₃} →
        ⟨ S₁ , s₁ ⟩⟶⟨ S₂ , s₂ ⟩  →  ⟨ S₂ , s₂ ⟩ k ⟶[ S₃ , s₃ ]
      → --------------------------------------------------------
                    ⟨ S₁ , s₁ ⟩ suc k ⟶[ S₃ , s₃ ]

-- Example program derivation (very slow to check!)
private
  prog : St 3
  prog =
    # 2 := lit 0 ,
    while lte (var (# 1)) (var (# 0)) do
      ( # 2 := add (var (# 2)) (lit 1) ,
        # 0 := sub (var (# 0)) (var (# 1)) )

  -- -- Uncomment if you dare
  -- prog-deriv :
  --   ∀ {z} → ⟨ prog , 17 ∷ 5 ∷ z ∷ [] ⟩ _ ⟶ (2 ∷ 5 ∷ 3 ∷ [])
  -- prog-deriv =
  --   ass ∙ ∷
  --     while ∷ if-true tt ∷ ass ∙ ◄ ∷ ass ∙ ∷
  --     while ∷ if-true tt ∷ ass ∙ ◄ ∷ ass ∙ ∷
  --     while ∷ if-true tt ∷ ass ∙ ◄ ∷ ass ∙ ∷
  --     while ∷ if-false tt ∷ skip stop

-- Divergence

_divergesOnₛ_ : ∀ {n} → St n → State n → Set
prog divergesOnₛ s = ∀ {n s'} → ¬ ⟨ prog , s ⟩ n ⟶ s'

Divergentₛ : ∀ {n} → St n → Set
Divergentₛ prog = ∀ {s} → prog divergesOnₛ s

private
  inf-loopₛ : ∀ {n} → Divergentₛ {n} (while tt do skip)
  inf-loopₛ (() stop)
  inf-loopₛ (while ∷ (() stop))
  inf-loopₛ (while ∷ (if-true tt ∷ (() stop)))
  inf-loopₛ (while ∷ (if-true tt ∷ ((() ◄) ∷ p)))
  inf-loopₛ (while ∷ (if-true tt ∷ ((skip ∙) ∷ p))) = inf-loopₛ p
  inf-loopₛ (while ∷ (if-false () ∷ p))

deterministicₛ :
  ∀ {n}{S : St n}{S' S'' s s' s''}
  → ⟨ S , s ⟩⟶[ S' , s' ] → ⟨ S , s ⟩⟶[ S'' , s'' ]
  → S' ≡ S'' × s' ≡ s''
deterministicₛ {n} = go where
  go : ∀ {S : St n}{S' S'' s s' s''}
      → ⟨ S , s ⟩⟶[ S' , s' ] → ⟨ S , s ⟩⟶[ S'' , s'' ]
      → S' ≡ S'' × s' ≡ s''
  go ass ass = refl , refl
  go skip skip = refl , refl
  go (p1 ◄) (p2 ◄) with go p1 p2
  ... | refl , refl = refl , refl
  go (p1 ◄) (p2 ∙) with go p1 p2
  ... | () , _
  go (p1 ∙) (p2 ◄) with go p1 p2
  ... | () , _
  go (p1 ∙) (p2 ∙) with go p1 p2
  ... | refl , refl = refl , refl
  go (if-true x) (if-true x₁) = refl , refl
  go (if-true x) (if-false x₁) rewrite T→≡true x = ⊥-elim x₁
  go (if-false x) (if-true x₁) rewrite T→≡true x₁ = ⊥-elim x
  go (if-false x) (if-false x₁) = refl , refl
  go while while = refl , refl

{-
Lemma 2.19 of the book: if we have a derivation over the composition of statements,
then there exists two derivations over the substatements, such that their lenghts
add up to the length of the original derivation.
-}

seq-split :
  ∀ {n k S₁ S₂}{s₁ s₃ : State n}
  → ⟨ (S₁ , S₂) , s₁ ⟩ k ⟶ s₃
  → Σ (State n × ℕ × ℕ) λ {(s₂ , k₁ , k₂)
  → ⟨ S₁ , s₁ ⟩ k₁ ⟶ s₂
  × ⟨ S₂ , s₂ ⟩ k₂ ⟶ s₃
  × k₁ + k₂ ≡ k}
seq-split (() stop)
seq-split (x ◄ ∷ p) with seq-split p
... | _ , p1 , p2 , prf = _ , x ∷ p1 , p2 , cong suc prf
seq-split (x ∙ ∷ p) = _ , x stop , p , refl

{-
Exercise 2.20.
-}
ex2-20 :
  ∃ λ n → ∃₂ λ (s s' : State n) → ∃₂ λ A B →
  ⟨ (A , B) , s ⟩⟶*⟨ B , s' ⟩ × ¬ ⟨ A , s ⟩⟶* s'
ex2-20 = 1 , (0 ∷ []) , (2 ∷ []) , A , (while b do A) , Deriv , ¬Deriv
  where
  A = zero := add (lit 1) (var zero)
  b = lt (var zero) (lit 2)
  Deriv = , ass ∙ ∷ while ∷ if-true tt ∷ ass ∙ ∷ pause
  ¬Deriv : ¬ ⟨ A , 0 ∷ [] ⟩⟶* (2 ∷ [])
  ¬Deriv (._ , () stop)
  ¬Deriv (._ , () ∷ proj₂)

{-
The converse of seq-split: two derivations can be appended to a single derivation
over the composition of the programs.
-}
append :
  ∀ {n k₁ k₂}{s s' s'' : State n}{A B}
  → ⟨ A , s ⟩ k₁ ⟶ s'
  → ⟨ B , s' ⟩ k₂ ⟶ s''
  → ⟨ (A , B) , s ⟩ (k₁ + k₂) ⟶ s''
append (x stop) p2 = (x ∙) ∷ p2
append (x ∷ p1) p2 = (x ◄) ∷ append p1 p2

-- Correctness of factorial (exactly the same proof as with big-step semantics)
private

  ⟦fac⟧ : ℕ → ℕ
  ⟦fac⟧ zero    = 1
  ⟦fac⟧ (suc n) = suc n * ⟦fac⟧ n

  fac-loop : St 3
  fac-loop =
    while lt (var (# 1)) (var (# 0)) do
      ( # 1 := add (lit 1) (var (# 1)) ,
        # 2 := mul (var (# 1)) (var (# 2)) )

  fac : St 3
  fac =
    # 1 := lit 0 ,
    # 2 := lit 1 ,
    fac-loop

  fac-loop-ok :
    ∀ d i → ⟨ fac-loop , d + i ∷ i ∷ ⟦fac⟧ i ∷ [] ⟩⟶* (d + i ∷ d + i ∷ ⟦fac⟧ (d + i) ∷ [])
  fac-loop-ok zero i =
    , while ∷ if-false (¬A→FalseA $ a≮a i) ∷ skip stop
  fac-loop-ok (suc d) i with fac-loop-ok d (suc i)
  ... | _ , next rewrite +-suc d i =
    , while ∷ if-true (A→TrueA $ a<sb+a i d) ∷ ass ∙ ◄ ∷ ass ∙ ∷ next

  fac-ok :
    ∀ n {i lim} → ⟨ fac , n ∷ i ∷ lim ∷ [] ⟩⟶* (n ∷ n ∷ ⟦fac⟧ n ∷ [])
  fac-ok n with fac-loop-ok n 0
  ... | _ , loop-ok rewrite +-comm n 0 = , ass ∙ ∷ ass ∙ ∷ loop-ok

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
-- Andreas, 2015-09-18 Andreas, reported by Andrea
-- {-# OPTIONS -v impossible:10 #-}
-- {-# OPTIONS -v tc.cover.splittree:10 #-}
-- {-# OPTIONS -v tc.cc:30 #-}

open import Common.Bool
open import Common.Product
open import Common.Equality

postulate
 A : Set
 a : A

Works : A × A → Bool → A
Works (x , y) true = y
Works d false = a

works : ∀{x y} → Works (x , y) false ≡ a
works = refl

Test : A × (A × A) → Bool → A
Test (x , (y , z)) true = z
Test d false = a

test : ∀{x y z} → Test (x , (y , z)) false ≡ a
test = refl

-- ERROR WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/CompiledClause/Match.hs:189

-- Behavior of clause compiler WAS:
-- splitting on 0 after expandCatchAlls True:
--   (x,(y,z)) true -> z
--   (_,_)     false -> a
--   _         false -> a
-- splitting on 1 after expandCatchAlls False:
--   d false -> a
-- splitting on 1 after expandCatchAlls False:  <== NOW: True
--   x (y,z) true  -> z
--   _ (_,_) false -> a  <== WAS MISSING
--   _ _     false -> a
-- splitting on 2 after expandCatchAlls False:
--   _ _ false -> a
-- splitting on 3 after expandCatchAlls False:
--   x y z true  -> z
--   x y z false -> a  <== WAS MISSING

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2013-10-30
-- Test whether verbosity options are honored before file is loaded.
-- See Issue641.flags

module Issue641 where

-- Provoke a scope checking error.

open NoSuchModule

-- Expected output is some debug messages about importing, plus the error,
-- like:

--   Getting interface for Issue641
--   Check for cycle
--   Issue641 is not up-to-date.
-- Creating interface for Issue641.
--   visited:
-- Issue641.agda:9,6-18
-- No such module NoSuchModule
-- when scope checking the declaration
--   open NoSuchModule


text:
{-# OPTIONS --no-positivity-check #-}

module STLC.Coquand.Completeness where

open import STLC.Coquand.Normalisation public
open import STLC.Coquand.Convertibility public

--------------------------------------------------------------------------------

data CV : ∀ {Γ A} → Γ ⊢ A → Γ ⊩ A → Set
  where
    cv⎵ : ∀ {Γ} → {M : Γ ⊢ ⎵} {f : Γ ⊩ ⎵}
                → (h : ∀ {Γ′} → (η : Γ′ ∋⋆ Γ)
                               → sub ⌊ η ⌋ M ∼ ⟦g⟧⟨ η ⟩ f)
                → CV M f

    cv⊃ : ∀ {Γ A B} → {M : Γ ⊢ A ⇒ B} {f : Γ ⊩ A ⇒ B}
                    → (h : ∀ {Γ′ N a} → (η : Γ′ ∋⋆ Γ) → CV N a
                                       → CV (sub ⌊ η ⌋ M ∙ N) (f ⟦∙⟧⟨ η ⟩ a))
                    → CV M f

data CV⋆ : ∀ {Γ Ξ} → Γ ⊢⋆ Ξ → Γ ⊩⋆ Ξ → Set
  where
    ∅   : ∀ {Γ} → {σ : Γ ⊢⋆ ∅}
                → CV⋆ σ ∅

    _,_ : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ , A} {ρ : Γ ⊩⋆ Ξ} {a : Γ ⊩ A}
                    → (κ : CV⋆ (σ ◐ wkᵣ {A} idᵣ) ρ) (k : CV (sub σ 0) a)
                    → CV⋆ σ (ρ , a)

--------------------------------------------------------------------------------

postulate
  congCV : ∀ {Γ A} → {M₁ M₂ : Γ ⊢ A} {a : Γ ⊩ A}
                   → M₁ ∼ M₂ → CV M₁ a
                   → CV M₂ a

-- (cong↑⟨_⟩CV)
postulate
  accCV : ∀ {Γ Γ′ A} → {M : Γ ⊢ A} {a : Γ ⊩ A}
                     → (η : Γ′ ∋⋆ Γ) → CV M a
                     → CV (sub ⌊ η ⌋ M) (acc η a)

-- (conglookupCV)
postulate
  getCV : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ⊩⋆ Ξ}
                    → (i : Ξ ∋ A) → CV⋆ σ ρ
                    → CV (sub σ (𝓋 i)) (getᵥ ρ i)

-- (cong↑⟨_⟩CV⋆)
postulate
  accCV⋆ : ∀ {Γ Γ′ Ξ} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ⊩⋆ Ξ}
                      → (η : Γ′ ∋⋆ Γ) → CV⋆ σ ρ
                      → CV⋆ (η ◑ σ) (η ⬗ ρ)

-- (cong↓⟨_⟩CV⋆)
postulate
  getCV⋆ : ∀ {Γ Ξ Ξ′} → {σ : Γ ⊢⋆ Ξ′} {ρ : Γ ⊩⋆ Ξ′}
                      → (η : Ξ′ ∋⋆ Ξ) → CV⋆ σ ρ
                      → CV⋆ (σ ◐ η) (ρ ⬖ η)

--------------------------------------------------------------------------------

-- Lemma 8.
postulate
  ⟦_⟧CV : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ⊩⋆ Ξ}
                    → (M : Ξ ⊢ A) → CV⋆ σ ρ
                    → CV (sub σ M) (⟦ M ⟧ ρ)

postulate
  ⟦_⟧CV⋆ : ∀ {Γ Ξ Φ} → {σ₁ : Γ ⊢⋆ Ξ} {ρ : Γ ⊩⋆ Ξ}
                     → (σ₂ : Ξ ⊢⋆ Φ) → CV⋆ σ₁ ρ
                     → CV⋆ (σ₁ ● σ₂) (⟦ σ₂ ⟧⋆ ρ)

--------------------------------------------------------------------------------

-- Lemma 9.
mutual
  postulate
    lem₉ : ∀ {Γ A} → {M : Γ ⊢ A} {a : Γ ⊩ A}
                   → CV M a
                   → M ∼ reify a

  postulate
    aux₄₆₈ : ∀ {A Γ} → {M : Γ ⊢ A} {f : ∀ {Γ′} → Γ′ ∋⋆ Γ → Γ′ ⊢ A}
                     → (∀ {Γ′} → (η : Γ′ ∋⋆ Γ) → sub ⌊ η ⌋ M ∼ f η)
                     → CV M (⟪ f ⟫)

postulate
  ⌊_⌋CV⋆ : ∀ {Γ Γ′} → (η : Γ′ ∋⋆ Γ)
                   → CV⋆ ⌊ η ⌋ ⌊ η ⌋ᵥ

idCV⋆ : ∀ {Γ} → CV⋆ ⌊ idᵣ ⌋ (idᵥ {Γ})
idCV⋆ = ⌊ idᵣ ⌋CV⋆

postulate
  aux₄₆₉ : ∀ {Γ A} → (M : Γ ⊢ A)
                   → sub ⌊ idᵣ ⌋ M ∼ nf M

--------------------------------------------------------------------------------

-- Theorem 2.
postulate
  thm₂ : ∀ {Γ A} → (M : Γ ⊢ A)
                 → M ∼ nf M

-- Theorem 3.
thm₃ : ∀ {Γ A} → (M₁ M₂ : Γ ⊢ A) → Eq (⟦ M₁ ⟧ idᵥ) (⟦ M₂ ⟧ idᵥ)
               → M₁ ∼ M₂
thm₃ M₁ M₂ e = thm₂ M₁
             ⦙ ≡→∼ (cor₁ M₁ M₂ e)
             ⦙ thm₂ M₂ ⁻¹

--------------------------------------------------------------------------------

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
{-# OPTIONS --warning=error #-}

module UselessPrivatePragma where

postulate Char : Set

private
  {-# BUILTIN CHAR Char #-}