1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
| infixr 2 _≈j₂_
data _≈j₂_ {A : Set} : CoList (Maybe A) → CoList (Maybe A) → Set where
nil : [] ≈j₂ []
noneb : ∀ {xs ys} → ∞ ( ♭ xs ≈j₂ ♭ ys) → nothing ∷ xs ≈j₂ nothing ∷ ys
nonel : ∀ {x xs ys} → ∞ ( ♭ xs ≈j₂ just x ∷ ys) → nothing ∷ xs ≈j₂ just x ∷ ys
noner : ∀ {x xs ys} → ∞ (just x ∷ xs ≈j₂ ♭ ys) → just x ∷ xs ≈j₂ nothing ∷ ys
justs : ∀ {x xs ys} → ∞ ( ♭ xs ≈j₂ ♭ ys) → just x ∷ xs ≈j₂ just x ∷ ys
≈j₂trans : ∀ {A} {xs ys zs : CoList (Maybe A)} → xs ≈j₂ ys → ys ≈j₂ zs → xs ≈j₂ zs
≈j₂trans nil nil = nil
≈j₂trans (noneb t₁) (noneb t₂) = noneb (♯ ≈j₂trans (♭ t₁) (♭ t₂))
≈j₂trans (noneb t₁) (nonel t₂) = nonel (♯ ≈j₂trans (♭ t₁) (♭ t₂))
≈j₂trans (nonel t₁) (noner t₂) = noneb (♯ ≈j₂trans (♭ t₁) (♭ t₂))
≈j₂trans (nonel t₁) (justs t₂) = nonel (♯ ≈j₂trans (♭ t₁) (justs t₂))
≈j₂trans (noner t₁) (noneb t₂) = noner (♯ ≈j₂trans (♭ t₁) (♭ t₂))
≈j₂trans (noner t₁) (nonel t₃) = {!!}
≈j₂trans (justs t₁) (noner t₂) = noner (♯ ≈j₂trans (justs t₁) (♭ t₂))
≈j₂trans (justs t₁) (justs t₂) = justs (♯ ≈j₂trans (♭ t₁) (♭ t₂))
|