text:
module Text.Greek.SBLGNT.2Tim where

open import Data.List
open import Text.Greek.Bible
open import Text.Greek.Script
open import Text.Greek.Script.Unicode

ΠΡΟΣ-ΤΙΜΟΘΕΟΝ-Β : List (Word)
ΠΡΟΣ-ΤΙΜΟΘΕΟΝ-Β =
    word (Π ∷ α ∷ ῦ ∷ ∙λ ∷ ο ∷ ς ∷ []) "2Tim.1.1"
  ∷ word (ἀ ∷ π ∷ ό ∷ σ ∷ τ ∷ ο ∷ ∙λ ∷ ο ∷ ς ∷ []) "2Tim.1.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.1.1"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Tim.1.1"
  ∷ word (θ ∷ ε ∷ ∙λ ∷ ή ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.1.1"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Tim.1.1"
  ∷ word (κ ∷ α ∷ τ ∷ []) "2Tim.1.1"
  ∷ word (ἐ ∷ π ∷ α ∷ γ ∷ γ ∷ ε ∷ ∙λ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.1.1"
  ∷ word (ζ ∷ ω ∷ ῆ ∷ ς ∷ []) "2Tim.1.1"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.1.1"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "2Tim.1.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.1.1"
  ∷ word (Τ ∷ ι ∷ μ ∷ ο ∷ θ ∷ έ ∷ ῳ ∷ []) "2Tim.1.2"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ ῷ ∷ []) "2Tim.1.2"
  ∷ word (τ ∷ έ ∷ κ ∷ ν ∷ ῳ ∷ []) "2Tim.1.2"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "2Tim.1.2"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ ο ∷ ς ∷ []) "2Tim.1.2"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ []) "2Tim.1.2"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Tim.1.2"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Tim.1.2"
  ∷ word (π ∷ α ∷ τ ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Tim.1.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.2"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.2"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.1.2"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.2"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.1.2"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Tim.1.2"
  ∷ word (Χ ∷ ά ∷ ρ ∷ ι ∷ ν ∷ []) "2Tim.1.3"
  ∷ word (ἔ ∷ χ ∷ ω ∷ []) "2Tim.1.3"
  ∷ word (τ ∷ ῷ ∷ []) "2Tim.1.3"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "2Tim.1.3"
  ∷ word (ᾧ ∷ []) "2Tim.1.3"
  ∷ word (∙λ ∷ α ∷ τ ∷ ρ ∷ ε ∷ ύ ∷ ω ∷ []) "2Tim.1.3"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Tim.1.3"
  ∷ word (π ∷ ρ ∷ ο ∷ γ ∷ ό ∷ ν ∷ ω ∷ ν ∷ []) "2Tim.1.3"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.3"
  ∷ word (κ ∷ α ∷ θ ∷ α ∷ ρ ∷ ᾷ ∷ []) "2Tim.1.3"
  ∷ word (σ ∷ υ ∷ ν ∷ ε ∷ ι ∷ δ ∷ ή ∷ σ ∷ ε ∷ ι ∷ []) "2Tim.1.3"
  ∷ word (ὡ ∷ ς ∷ []) "2Tim.1.3"
  ∷ word (ἀ ∷ δ ∷ ι ∷ ά ∷ ∙λ ∷ ε ∷ ι ∷ π ∷ τ ∷ ο ∷ ν ∷ []) "2Tim.1.3"
  ∷ word (ἔ ∷ χ ∷ ω ∷ []) "2Tim.1.3"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.1.3"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "2Tim.1.3"
  ∷ word (σ ∷ ο ∷ ῦ ∷ []) "2Tim.1.3"
  ∷ word (μ ∷ ν ∷ ε ∷ ί ∷ α ∷ ν ∷ []) "2Tim.1.3"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.3"
  ∷ word (τ ∷ α ∷ ῖ ∷ ς ∷ []) "2Tim.1.3"
  ∷ word (δ ∷ ε ∷ ή ∷ σ ∷ ε ∷ σ ∷ ί ∷ ν ∷ []) "2Tim.1.3"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "2Tim.1.3"
  ∷ word (ν ∷ υ ∷ κ ∷ τ ∷ ὸ ∷ ς ∷ []) "2Tim.1.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.3"
  ∷ word (ἡ ∷ μ ∷ έ ∷ ρ ∷ α ∷ ς ∷ []) "2Tim.1.3"
  ∷ word (ἐ ∷ π ∷ ι ∷ π ∷ ο ∷ θ ∷ ῶ ∷ ν ∷ []) "2Tim.1.4"
  ∷ word (σ ∷ ε ∷ []) "2Tim.1.4"
  ∷ word (ἰ ∷ δ ∷ ε ∷ ῖ ∷ ν ∷ []) "2Tim.1.4"
  ∷ word (μ ∷ ε ∷ μ ∷ ν ∷ η ∷ μ ∷ έ ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.1.4"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "2Tim.1.4"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "2Tim.1.4"
  ∷ word (δ ∷ α ∷ κ ∷ ρ ∷ ύ ∷ ω ∷ ν ∷ []) "2Tim.1.4"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Tim.1.4"
  ∷ word (χ ∷ α ∷ ρ ∷ ᾶ ∷ ς ∷ []) "2Tim.1.4"
  ∷ word (π ∷ ∙λ ∷ η ∷ ρ ∷ ω ∷ θ ∷ ῶ ∷ []) "2Tim.1.4"
  ∷ word (ὑ ∷ π ∷ ό ∷ μ ∷ ν ∷ η ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.1.5"
  ∷ word (∙λ ∷ α ∷ β ∷ ὼ ∷ ν ∷ []) "2Tim.1.5"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.1.5"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.5"
  ∷ word (σ ∷ ο ∷ ὶ ∷ []) "2Tim.1.5"
  ∷ word (ἀ ∷ ν ∷ υ ∷ π ∷ ο ∷ κ ∷ ρ ∷ ί ∷ τ ∷ ο ∷ υ ∷ []) "2Tim.1.5"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ω ∷ ς ∷ []) "2Tim.1.5"
  ∷ word (ἥ ∷ τ ∷ ι ∷ ς ∷ []) "2Tim.1.5"
  ∷ word (ἐ ∷ ν ∷ ῴ ∷ κ ∷ η ∷ σ ∷ ε ∷ ν ∷ []) "2Tim.1.5"
  ∷ word (π ∷ ρ ∷ ῶ ∷ τ ∷ ο ∷ ν ∷ []) "2Tim.1.5"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.5"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.1.5"
  ∷ word (μ ∷ ά ∷ μ ∷ μ ∷ ῃ ∷ []) "2Tim.1.5"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "2Tim.1.5"
  ∷ word (Λ ∷ ω ∷ ΐ ∷ δ ∷ ι ∷ []) "2Tim.1.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.5"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.1.5"
  ∷ word (μ ∷ η ∷ τ ∷ ρ ∷ ί ∷ []) "2Tim.1.5"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "2Tim.1.5"
  ∷ word (Ε ∷ ὐ ∷ ν ∷ ί ∷ κ ∷ ῃ ∷ []) "2Tim.1.5"
  ∷ word (π ∷ έ ∷ π ∷ ε ∷ ι ∷ σ ∷ μ ∷ α ∷ ι ∷ []) "2Tim.1.5"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.1.5"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Tim.1.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.5"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.5"
  ∷ word (σ ∷ ο ∷ ί ∷ []) "2Tim.1.5"
  ∷ word (δ ∷ ι ∷ []) "2Tim.1.6"
  ∷ word (ἣ ∷ ν ∷ []) "2Tim.1.6"
  ∷ word (α ∷ ἰ ∷ τ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.1.6"
  ∷ word (ἀ ∷ ν ∷ α ∷ μ ∷ ι ∷ μ ∷ ν ∷ ῄ ∷ σ ∷ κ ∷ ω ∷ []) "2Tim.1.6"
  ∷ word (σ ∷ ε ∷ []) "2Tim.1.6"
  ∷ word (ἀ ∷ ν ∷ α ∷ ζ ∷ ω ∷ π ∷ υ ∷ ρ ∷ ε ∷ ῖ ∷ ν ∷ []) "2Tim.1.6"
  ∷ word (τ ∷ ὸ ∷ []) "2Tim.1.6"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ σ ∷ μ ∷ α ∷ []) "2Tim.1.6"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.6"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Tim.1.6"
  ∷ word (ὅ ∷ []) "2Tim.1.6"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.1.6"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.6"
  ∷ word (σ ∷ ο ∷ ὶ ∷ []) "2Tim.1.6"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Tim.1.6"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.1.6"
  ∷ word (ἐ ∷ π ∷ ι ∷ θ ∷ έ ∷ σ ∷ ε ∷ ω ∷ ς ∷ []) "2Tim.1.6"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "2Tim.1.6"
  ∷ word (χ ∷ ε ∷ ι ∷ ρ ∷ ῶ ∷ ν ∷ []) "2Tim.1.6"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "2Tim.1.6"
  ∷ word (ο ∷ ὐ ∷ []) "2Tim.1.7"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Tim.1.7"
  ∷ word (ἔ ∷ δ ∷ ω ∷ κ ∷ ε ∷ ν ∷ []) "2Tim.1.7"
  ∷ word (ἡ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Tim.1.7"
  ∷ word (ὁ ∷ []) "2Tim.1.7"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ς ∷ []) "2Tim.1.7"
  ∷ word (π ∷ ν ∷ ε ∷ ῦ ∷ μ ∷ α ∷ []) "2Tim.1.7"
  ∷ word (δ ∷ ε ∷ ι ∷ ∙λ ∷ ί ∷ α ∷ ς ∷ []) "2Tim.1.7"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.1.7"
  ∷ word (δ ∷ υ ∷ ν ∷ ά ∷ μ ∷ ε ∷ ω ∷ ς ∷ []) "2Tim.1.7"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.7"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ η ∷ ς ∷ []) "2Tim.1.7"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.7"
  ∷ word (σ ∷ ω ∷ φ ∷ ρ ∷ ο ∷ ν ∷ ι ∷ σ ∷ μ ∷ ο ∷ ῦ ∷ []) "2Tim.1.7"
  ∷ word (Μ ∷ ὴ ∷ []) "2Tim.1.8"
  ∷ word (ο ∷ ὖ ∷ ν ∷ []) "2Tim.1.8"
  ∷ word (ἐ ∷ π ∷ α ∷ ι ∷ σ ∷ χ ∷ υ ∷ ν ∷ θ ∷ ῇ ∷ ς ∷ []) "2Tim.1.8"
  ∷ word (τ ∷ ὸ ∷ []) "2Tim.1.8"
  ∷ word (μ ∷ α ∷ ρ ∷ τ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ν ∷ []) "2Tim.1.8"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.8"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.1.8"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Tim.1.8"
  ∷ word (μ ∷ η ∷ δ ∷ ὲ ∷ []) "2Tim.1.8"
  ∷ word (ἐ ∷ μ ∷ ὲ ∷ []) "2Tim.1.8"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.1.8"
  ∷ word (δ ∷ έ ∷ σ ∷ μ ∷ ι ∷ ο ∷ ν ∷ []) "2Tim.1.8"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.8"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.1.8"
  ∷ word (σ ∷ υ ∷ γ ∷ κ ∷ α ∷ κ ∷ ο ∷ π ∷ ά ∷ θ ∷ η ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.1.8"
  ∷ word (τ ∷ ῷ ∷ []) "2Tim.1.8"
  ∷ word (ε ∷ ὐ ∷ α ∷ γ ∷ γ ∷ ε ∷ ∙λ ∷ ί ∷ ῳ ∷ []) "2Tim.1.8"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2Tim.1.8"
  ∷ word (δ ∷ ύ ∷ ν ∷ α ∷ μ ∷ ι ∷ ν ∷ []) "2Tim.1.8"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Tim.1.8"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.9"
  ∷ word (σ ∷ ώ ∷ σ ∷ α ∷ ν ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.1.9"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Tim.1.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.9"
  ∷ word (κ ∷ α ∷ ∙λ ∷ έ ∷ σ ∷ α ∷ ν ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.1.9"
  ∷ word (κ ∷ ∙λ ∷ ή ∷ σ ∷ ε ∷ ι ∷ []) "2Tim.1.9"
  ∷ word (ἁ ∷ γ ∷ ί ∷ ᾳ ∷ []) "2Tim.1.9"
  ∷ word (ο ∷ ὐ ∷ []) "2Tim.1.9"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2Tim.1.9"
  ∷ word (τ ∷ ὰ ∷ []) "2Tim.1.9"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ α ∷ []) "2Tim.1.9"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.1.9"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2Tim.1.9"
  ∷ word (ἰ ∷ δ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (π ∷ ρ ∷ ό ∷ θ ∷ ε ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.9"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (δ ∷ ο ∷ θ ∷ ε ∷ ῖ ∷ σ ∷ α ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (ἡ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "2Tim.1.9"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.1.9"
  ∷ word (π ∷ ρ ∷ ὸ ∷ []) "2Tim.1.9"
  ∷ word (χ ∷ ρ ∷ ό ∷ ν ∷ ω ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (α ∷ ἰ ∷ ω ∷ ν ∷ ί ∷ ω ∷ ν ∷ []) "2Tim.1.9"
  ∷ word (φ ∷ α ∷ ν ∷ ε ∷ ρ ∷ ω ∷ θ ∷ ε ∷ ῖ ∷ σ ∷ α ∷ ν ∷ []) "2Tim.1.10"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.1.10"
  ∷ word (ν ∷ ῦ ∷ ν ∷ []) "2Tim.1.10"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Tim.1.10"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.1.10"
  ∷ word (ἐ ∷ π ∷ ι ∷ φ ∷ α ∷ ν ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Tim.1.10"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.10"
  ∷ word (σ ∷ ω ∷ τ ∷ ῆ ∷ ρ ∷ ο ∷ ς ∷ []) "2Tim.1.10"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Tim.1.10"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.1.10"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.10"
  ∷ word (κ ∷ α ∷ τ ∷ α ∷ ρ ∷ γ ∷ ή ∷ σ ∷ α ∷ ν ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.1.10"
  ∷ word (μ ∷ ὲ ∷ ν ∷ []) "2Tim.1.10"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.1.10"
  ∷ word (θ ∷ ά ∷ ν ∷ α ∷ τ ∷ ο ∷ ν ∷ []) "2Tim.1.10"
  ∷ word (φ ∷ ω ∷ τ ∷ ί ∷ σ ∷ α ∷ ν ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.1.10"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.1.10"
  ∷ word (ζ ∷ ω ∷ ὴ ∷ ν ∷ []) "2Tim.1.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.10"
  ∷ word (ἀ ∷ φ ∷ θ ∷ α ∷ ρ ∷ σ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.1.10"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Tim.1.10"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.10"
  ∷ word (ε ∷ ὐ ∷ α ∷ γ ∷ γ ∷ ε ∷ ∙λ ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.1.10"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.1.11"
  ∷ word (ὃ ∷ []) "2Tim.1.11"
  ∷ word (ἐ ∷ τ ∷ έ ∷ θ ∷ η ∷ ν ∷ []) "2Tim.1.11"
  ∷ word (ἐ ∷ γ ∷ ὼ ∷ []) "2Tim.1.11"
  ∷ word (κ ∷ ῆ ∷ ρ ∷ υ ∷ ξ ∷ []) "2Tim.1.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.11"
  ∷ word (ἀ ∷ π ∷ ό ∷ σ ∷ τ ∷ ο ∷ ∙λ ∷ ο ∷ ς ∷ []) "2Tim.1.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.11"
  ∷ word (δ ∷ ι ∷ δ ∷ ά ∷ σ ∷ κ ∷ α ∷ ∙λ ∷ ο ∷ ς ∷ []) "2Tim.1.11"
  ∷ word (δ ∷ ι ∷ []) "2Tim.1.12"
  ∷ word (ἣ ∷ ν ∷ []) "2Tim.1.12"
  ∷ word (α ∷ ἰ ∷ τ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.1.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.12"
  ∷ word (τ ∷ α ∷ ῦ ∷ τ ∷ α ∷ []) "2Tim.1.12"
  ∷ word (π ∷ ά ∷ σ ∷ χ ∷ ω ∷ []) "2Tim.1.12"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ []) "2Tim.1.12"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2Tim.1.12"
  ∷ word (ἐ ∷ π ∷ α ∷ ι ∷ σ ∷ χ ∷ ύ ∷ ν ∷ ο ∷ μ ∷ α ∷ ι ∷ []) "2Tim.1.12"
  ∷ word (ο ∷ ἶ ∷ δ ∷ α ∷ []) "2Tim.1.12"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Tim.1.12"
  ∷ word (ᾧ ∷ []) "2Tim.1.12"
  ∷ word (π ∷ ε ∷ π ∷ ί ∷ σ ∷ τ ∷ ε ∷ υ ∷ κ ∷ α ∷ []) "2Tim.1.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.12"
  ∷ word (π ∷ έ ∷ π ∷ ε ∷ ι ∷ σ ∷ μ ∷ α ∷ ι ∷ []) "2Tim.1.12"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Tim.1.12"
  ∷ word (δ ∷ υ ∷ ν ∷ α ∷ τ ∷ ό ∷ ς ∷ []) "2Tim.1.12"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.1.12"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.1.12"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ θ ∷ ή ∷ κ ∷ η ∷ ν ∷ []) "2Tim.1.12"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "2Tim.1.12"
  ∷ word (φ ∷ υ ∷ ∙λ ∷ ά ∷ ξ ∷ α ∷ ι ∷ []) "2Tim.1.12"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.1.12"
  ∷ word (ἐ ∷ κ ∷ ε ∷ ί ∷ ν ∷ η ∷ ν ∷ []) "2Tim.1.12"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.1.12"
  ∷ word (ἡ ∷ μ ∷ έ ∷ ρ ∷ α ∷ ν ∷ []) "2Tim.1.12"
  ∷ word (ὑ ∷ π ∷ ο ∷ τ ∷ ύ ∷ π ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.1.13"
  ∷ word (ἔ ∷ χ ∷ ε ∷ []) "2Tim.1.13"
  ∷ word (ὑ ∷ γ ∷ ι ∷ α ∷ ι ∷ ν ∷ ό ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "2Tim.1.13"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ω ∷ ν ∷ []) "2Tim.1.13"
  ∷ word (ὧ ∷ ν ∷ []) "2Tim.1.13"
  ∷ word (π ∷ α ∷ ρ ∷ []) "2Tim.1.13"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ῦ ∷ []) "2Tim.1.13"
  ∷ word (ἤ ∷ κ ∷ ο ∷ υ ∷ σ ∷ α ∷ ς ∷ []) "2Tim.1.13"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.13"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ι ∷ []) "2Tim.1.13"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.13"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ ῃ ∷ []) "2Tim.1.13"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.1.13"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.13"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "2Tim.1.13"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.1.13"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.1.14"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ὴ ∷ ν ∷ []) "2Tim.1.14"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ θ ∷ ή ∷ κ ∷ η ∷ ν ∷ []) "2Tim.1.14"
  ∷ word (φ ∷ ύ ∷ ∙λ ∷ α ∷ ξ ∷ ο ∷ ν ∷ []) "2Tim.1.14"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Tim.1.14"
  ∷ word (π ∷ ν ∷ ε ∷ ύ ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.1.14"
  ∷ word (ἁ ∷ γ ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.1.14"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.1.14"
  ∷ word (ἐ ∷ ν ∷ ο ∷ ι ∷ κ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.1.14"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.14"
  ∷ word (ἡ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Tim.1.14"
  ∷ word (Ο ∷ ἶ ∷ δ ∷ α ∷ ς ∷ []) "2Tim.1.15"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "2Tim.1.15"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Tim.1.15"
  ∷ word (ἀ ∷ π ∷ ε ∷ σ ∷ τ ∷ ρ ∷ ά ∷ φ ∷ η ∷ σ ∷ ά ∷ ν ∷ []) "2Tim.1.15"
  ∷ word (μ ∷ ε ∷ []) "2Tim.1.15"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.1.15"
  ∷ word (ο ∷ ἱ ∷ []) "2Tim.1.15"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.15"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.1.15"
  ∷ word (Ἀ ∷ σ ∷ ί ∷ ᾳ ∷ []) "2Tim.1.15"
  ∷ word (ὧ ∷ ν ∷ []) "2Tim.1.15"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.1.15"
  ∷ word (Φ ∷ ύ ∷ γ ∷ ε ∷ ∙λ ∷ ο ∷ ς ∷ []) "2Tim.1.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.15"
  ∷ word (Ἑ ∷ ρ ∷ μ ∷ ο ∷ γ ∷ έ ∷ ν ∷ η ∷ ς ∷ []) "2Tim.1.15"
  ∷ word (δ ∷ ῴ ∷ η ∷ []) "2Tim.1.16"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ ο ∷ ς ∷ []) "2Tim.1.16"
  ∷ word (ὁ ∷ []) "2Tim.1.16"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.1.16"
  ∷ word (τ ∷ ῷ ∷ []) "2Tim.1.16"
  ∷ word (Ὀ ∷ ν ∷ η ∷ σ ∷ ι ∷ φ ∷ ό ∷ ρ ∷ ο ∷ υ ∷ []) "2Tim.1.16"
  ∷ word (ο ∷ ἴ ∷ κ ∷ ῳ ∷ []) "2Tim.1.16"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Tim.1.16"
  ∷ word (π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ά ∷ κ ∷ ι ∷ ς ∷ []) "2Tim.1.16"
  ∷ word (μ ∷ ε ∷ []) "2Tim.1.16"
  ∷ word (ἀ ∷ ν ∷ έ ∷ ψ ∷ υ ∷ ξ ∷ ε ∷ ν ∷ []) "2Tim.1.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.16"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.1.16"
  ∷ word (ἅ ∷ ∙λ ∷ υ ∷ σ ∷ ί ∷ ν ∷ []) "2Tim.1.16"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "2Tim.1.16"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2Tim.1.16"
  ∷ word (ἐ ∷ π ∷ α ∷ ι ∷ σ ∷ χ ∷ ύ ∷ ν ∷ θ ∷ η ∷ []) "2Tim.1.16"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.1.17"
  ∷ word (γ ∷ ε ∷ ν ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.1.17"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.17"
  ∷ word (Ῥ ∷ ώ ∷ μ ∷ ῃ ∷ []) "2Tim.1.17"
  ∷ word (σ ∷ π ∷ ο ∷ υ ∷ δ ∷ α ∷ ί ∷ ω ∷ ς ∷ []) "2Tim.1.17"
  ∷ word (ἐ ∷ ζ ∷ ή ∷ τ ∷ η ∷ σ ∷ έ ∷ ν ∷ []) "2Tim.1.17"
  ∷ word (μ ∷ ε ∷ []) "2Tim.1.17"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.17"
  ∷ word (ε ∷ ὗ ∷ ρ ∷ ε ∷ ν ∷ []) "2Tim.1.17"
  ∷ word (δ ∷ ῴ ∷ η ∷ []) "2Tim.1.18"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῷ ∷ []) "2Tim.1.18"
  ∷ word (ὁ ∷ []) "2Tim.1.18"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.1.18"
  ∷ word (ε ∷ ὑ ∷ ρ ∷ ε ∷ ῖ ∷ ν ∷ []) "2Tim.1.18"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ ο ∷ ς ∷ []) "2Tim.1.18"
  ∷ word (π ∷ α ∷ ρ ∷ ὰ ∷ []) "2Tim.1.18"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.1.18"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.18"
  ∷ word (ἐ ∷ κ ∷ ε ∷ ί ∷ ν ∷ ῃ ∷ []) "2Tim.1.18"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.1.18"
  ∷ word (ἡ ∷ μ ∷ έ ∷ ρ ∷ ᾳ ∷ []) "2Tim.1.18"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.1.18"
  ∷ word (ὅ ∷ σ ∷ α ∷ []) "2Tim.1.18"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.1.18"
  ∷ word (Ἐ ∷ φ ∷ έ ∷ σ ∷ ῳ ∷ []) "2Tim.1.18"
  ∷ word (δ ∷ ι ∷ η ∷ κ ∷ ό ∷ ν ∷ η ∷ σ ∷ ε ∷ ν ∷ []) "2Tim.1.18"
  ∷ word (β ∷ έ ∷ ∙λ ∷ τ ∷ ι ∷ ο ∷ ν ∷ []) "2Tim.1.18"
  ∷ word (σ ∷ ὺ ∷ []) "2Tim.1.18"
  ∷ word (γ ∷ ι ∷ ν ∷ ώ ∷ σ ∷ κ ∷ ε ∷ ι ∷ ς ∷ []) "2Tim.1.18"
  ∷ word (Σ ∷ ὺ ∷ []) "2Tim.2.1"
  ∷ word (ο ∷ ὖ ∷ ν ∷ []) "2Tim.2.1"
  ∷ word (τ ∷ έ ∷ κ ∷ ν ∷ ο ∷ ν ∷ []) "2Tim.2.1"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "2Tim.2.1"
  ∷ word (ἐ ∷ ν ∷ δ ∷ υ ∷ ν ∷ α ∷ μ ∷ ο ∷ ῦ ∷ []) "2Tim.2.1"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.2.1"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.2.1"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ τ ∷ ι ∷ []) "2Tim.2.1"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.2.1"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.2.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "2Tim.2.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.2.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.2"
  ∷ word (ἃ ∷ []) "2Tim.2.2"
  ∷ word (ἤ ∷ κ ∷ ο ∷ υ ∷ σ ∷ α ∷ ς ∷ []) "2Tim.2.2"
  ∷ word (π ∷ α ∷ ρ ∷ []) "2Tim.2.2"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ῦ ∷ []) "2Tim.2.2"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Tim.2.2"
  ∷ word (π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ῶ ∷ ν ∷ []) "2Tim.2.2"
  ∷ word (μ ∷ α ∷ ρ ∷ τ ∷ ύ ∷ ρ ∷ ω ∷ ν ∷ []) "2Tim.2.2"
  ∷ word (τ ∷ α ∷ ῦ ∷ τ ∷ α ∷ []) "2Tim.2.2"
  ∷ word (π ∷ α ∷ ρ ∷ ά ∷ θ ∷ ο ∷ υ ∷ []) "2Tim.2.2"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Tim.2.2"
  ∷ word (ἀ ∷ ν ∷ θ ∷ ρ ∷ ώ ∷ π ∷ ο ∷ ι ∷ ς ∷ []) "2Tim.2.2"
  ∷ word (ο ∷ ἵ ∷ τ ∷ ι ∷ ν ∷ ε ∷ ς ∷ []) "2Tim.2.2"
  ∷ word (ἱ ∷ κ ∷ α ∷ ν ∷ ο ∷ ὶ ∷ []) "2Tim.2.2"
  ∷ word (ἔ ∷ σ ∷ ο ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "2Tim.2.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.2"
  ∷ word (ἑ ∷ τ ∷ έ ∷ ρ ∷ ο ∷ υ ∷ ς ∷ []) "2Tim.2.2"
  ∷ word (δ ∷ ι ∷ δ ∷ ά ∷ ξ ∷ α ∷ ι ∷ []) "2Tim.2.2"
  ∷ word (σ ∷ υ ∷ γ ∷ κ ∷ α ∷ κ ∷ ο ∷ π ∷ ά ∷ θ ∷ η ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.2.3"
  ∷ word (ὡ ∷ ς ∷ []) "2Tim.2.3"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ὸ ∷ ς ∷ []) "2Tim.2.3"
  ∷ word (σ ∷ τ ∷ ρ ∷ α ∷ τ ∷ ι ∷ ώ ∷ τ ∷ η ∷ ς ∷ []) "2Tim.2.3"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.2.3"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.2.3"
  ∷ word (ο ∷ ὐ ∷ δ ∷ ε ∷ ὶ ∷ ς ∷ []) "2Tim.2.4"
  ∷ word (σ ∷ τ ∷ ρ ∷ α ∷ τ ∷ ε ∷ υ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.2.4"
  ∷ word (ἐ ∷ μ ∷ π ∷ ∙λ ∷ έ ∷ κ ∷ ε ∷ τ ∷ α ∷ ι ∷ []) "2Tim.2.4"
  ∷ word (τ ∷ α ∷ ῖ ∷ ς ∷ []) "2Tim.2.4"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.2.4"
  ∷ word (β ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.2.4"
  ∷ word (π ∷ ρ ∷ α ∷ γ ∷ μ ∷ α ∷ τ ∷ ε ∷ ί ∷ α ∷ ι ∷ ς ∷ []) "2Tim.2.4"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Tim.2.4"
  ∷ word (τ ∷ ῷ ∷ []) "2Tim.2.4"
  ∷ word (σ ∷ τ ∷ ρ ∷ α ∷ τ ∷ ο ∷ ∙λ ∷ ο ∷ γ ∷ ή ∷ σ ∷ α ∷ ν ∷ τ ∷ ι ∷ []) "2Tim.2.4"
  ∷ word (ἀ ∷ ρ ∷ έ ∷ σ ∷ ῃ ∷ []) "2Tim.2.4"
  ∷ word (ἐ ∷ ὰ ∷ ν ∷ []) "2Tim.2.5"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.2.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.5"
  ∷ word (ἀ ∷ θ ∷ ∙λ ∷ ῇ ∷ []) "2Tim.2.5"
  ∷ word (τ ∷ ι ∷ ς ∷ []) "2Tim.2.5"
  ∷ word (ο ∷ ὐ ∷ []) "2Tim.2.5"
  ∷ word (σ ∷ τ ∷ ε ∷ φ ∷ α ∷ ν ∷ ο ∷ ῦ ∷ τ ∷ α ∷ ι ∷ []) "2Tim.2.5"
  ∷ word (ἐ ∷ ὰ ∷ ν ∷ []) "2Tim.2.5"
  ∷ word (μ ∷ ὴ ∷ []) "2Tim.2.5"
  ∷ word (ν ∷ ο ∷ μ ∷ ί ∷ μ ∷ ω ∷ ς ∷ []) "2Tim.2.5"
  ∷ word (ἀ ∷ θ ∷ ∙λ ∷ ή ∷ σ ∷ ῃ ∷ []) "2Tim.2.5"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.2.6"
  ∷ word (κ ∷ ο ∷ π ∷ ι ∷ ῶ ∷ ν ∷ τ ∷ α ∷ []) "2Tim.2.6"
  ∷ word (γ ∷ ε ∷ ω ∷ ρ ∷ γ ∷ ὸ ∷ ν ∷ []) "2Tim.2.6"
  ∷ word (δ ∷ ε ∷ ῖ ∷ []) "2Tim.2.6"
  ∷ word (π ∷ ρ ∷ ῶ ∷ τ ∷ ο ∷ ν ∷ []) "2Tim.2.6"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "2Tim.2.6"
  ∷ word (κ ∷ α ∷ ρ ∷ π ∷ ῶ ∷ ν ∷ []) "2Tim.2.6"
  ∷ word (μ ∷ ε ∷ τ ∷ α ∷ ∙λ ∷ α ∷ μ ∷ β ∷ ά ∷ ν ∷ ε ∷ ι ∷ ν ∷ []) "2Tim.2.6"
  ∷ word (ν ∷ ό ∷ ε ∷ ι ∷ []) "2Tim.2.7"
  ∷ word (ὃ ∷ []) "2Tim.2.7"
  ∷ word (∙λ ∷ έ ∷ γ ∷ ω ∷ []) "2Tim.2.7"
  ∷ word (δ ∷ ώ ∷ σ ∷ ε ∷ ι ∷ []) "2Tim.2.7"
  ∷ word (γ ∷ ά ∷ ρ ∷ []) "2Tim.2.7"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "2Tim.2.7"
  ∷ word (ὁ ∷ []) "2Tim.2.7"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.2.7"
  ∷ word (σ ∷ ύ ∷ ν ∷ ε ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.2.7"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.2.7"
  ∷ word (π ∷ ᾶ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.2.7"
  ∷ word (Μ ∷ ν ∷ η ∷ μ ∷ ό ∷ ν ∷ ε ∷ υ ∷ ε ∷ []) "2Tim.2.8"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ ν ∷ []) "2Tim.2.8"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ὸ ∷ ν ∷ []) "2Tim.2.8"
  ∷ word (ἐ ∷ γ ∷ η ∷ γ ∷ ε ∷ ρ ∷ μ ∷ έ ∷ ν ∷ ο ∷ ν ∷ []) "2Tim.2.8"
  ∷ word (ἐ ∷ κ ∷ []) "2Tim.2.8"
  ∷ word (ν ∷ ε ∷ κ ∷ ρ ∷ ῶ ∷ ν ∷ []) "2Tim.2.8"
  ∷ word (ἐ ∷ κ ∷ []) "2Tim.2.8"
  ∷ word (σ ∷ π ∷ έ ∷ ρ ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.2.8"
  ∷ word (Δ ∷ α ∷ υ ∷ ί ∷ δ ∷ []) "2Tim.2.8"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2Tim.2.8"
  ∷ word (τ ∷ ὸ ∷ []) "2Tim.2.8"
  ∷ word (ε ∷ ὐ ∷ α ∷ γ ∷ γ ∷ έ ∷ ∙λ ∷ ι ∷ ό ∷ ν ∷ []) "2Tim.2.8"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "2Tim.2.8"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.2.9"
  ∷ word (ᾧ ∷ []) "2Tim.2.9"
  ∷ word (κ ∷ α ∷ κ ∷ ο ∷ π ∷ α ∷ θ ∷ ῶ ∷ []) "2Tim.2.9"
  ∷ word (μ ∷ έ ∷ χ ∷ ρ ∷ ι ∷ []) "2Tim.2.9"
  ∷ word (δ ∷ ε ∷ σ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Tim.2.9"
  ∷ word (ὡ ∷ ς ∷ []) "2Tim.2.9"
  ∷ word (κ ∷ α ∷ κ ∷ ο ∷ ῦ ∷ ρ ∷ γ ∷ ο ∷ ς ∷ []) "2Tim.2.9"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.2.9"
  ∷ word (ὁ ∷ []) "2Tim.2.9"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ς ∷ []) "2Tim.2.9"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.2.9"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Tim.2.9"
  ∷ word (ο ∷ ὐ ∷ []) "2Tim.2.9"
  ∷ word (δ ∷ έ ∷ δ ∷ ε ∷ τ ∷ α ∷ ι ∷ []) "2Tim.2.9"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Tim.2.10"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "2Tim.2.10"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ []) "2Tim.2.10"
  ∷ word (ὑ ∷ π ∷ ο ∷ μ ∷ έ ∷ ν ∷ ω ∷ []) "2Tim.2.10"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Tim.2.10"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Tim.2.10"
  ∷ word (ἐ ∷ κ ∷ ∙λ ∷ ε ∷ κ ∷ τ ∷ ο ∷ ύ ∷ ς ∷ []) "2Tim.2.10"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Tim.2.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.10"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ὶ ∷ []) "2Tim.2.10"
  ∷ word (σ ∷ ω ∷ τ ∷ η ∷ ρ ∷ ί ∷ α ∷ ς ∷ []) "2Tim.2.10"
  ∷ word (τ ∷ ύ ∷ χ ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.2.10"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.2.10"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.2.10"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "2Tim.2.10"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.2.10"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "2Tim.2.10"
  ∷ word (δ ∷ ό ∷ ξ ∷ η ∷ ς ∷ []) "2Tim.2.10"
  ∷ word (α ∷ ἰ ∷ ω ∷ ν ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.2.10"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ὸ ∷ ς ∷ []) "2Tim.2.11"
  ∷ word (ὁ ∷ []) "2Tim.2.11"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ς ∷ []) "2Tim.2.11"
  ∷ word (ε ∷ ἰ ∷ []) "2Tim.2.11"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Tim.2.11"
  ∷ word (σ ∷ υ ∷ ν ∷ α ∷ π ∷ ε ∷ θ ∷ ά ∷ ν ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Tim.2.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.11"
  ∷ word (σ ∷ υ ∷ ζ ∷ ή ∷ σ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Tim.2.11"
  ∷ word (ε ∷ ἰ ∷ []) "2Tim.2.12"
  ∷ word (ὑ ∷ π ∷ ο ∷ μ ∷ έ ∷ ν ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Tim.2.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.12"
  ∷ word (σ ∷ υ ∷ μ ∷ β ∷ α ∷ σ ∷ ι ∷ ∙λ ∷ ε ∷ ύ ∷ σ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Tim.2.12"
  ∷ word (ε ∷ ἰ ∷ []) "2Tim.2.12"
  ∷ word (ἀ ∷ ρ ∷ ν ∷ η ∷ σ ∷ ό ∷ μ ∷ ε ∷ θ ∷ α ∷ []) "2Tim.2.12"
  ∷ word (κ ∷ ἀ ∷ κ ∷ ε ∷ ῖ ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.2.12"
  ∷ word (ἀ ∷ ρ ∷ ν ∷ ή ∷ σ ∷ ε ∷ τ ∷ α ∷ ι ∷ []) "2Tim.2.12"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Tim.2.12"
  ∷ word (ε ∷ ἰ ∷ []) "2Tim.2.13"
  ∷ word (ἀ ∷ π ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ μ ∷ ε ∷ ν ∷ []) "2Tim.2.13"
  ∷ word (ἐ ∷ κ ∷ ε ∷ ῖ ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.2.13"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ὸ ∷ ς ∷ []) "2Tim.2.13"
  ∷ word (μ ∷ έ ∷ ν ∷ ε ∷ ι ∷ []) "2Tim.2.13"
  ∷ word (ἀ ∷ ρ ∷ ν ∷ ή ∷ σ ∷ α ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2Tim.2.13"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ὸ ∷ ν ∷ []) "2Tim.2.13"
  ∷ word (ο ∷ ὐ ∷ []) "2Tim.2.13"
  ∷ word (δ ∷ ύ ∷ ν ∷ α ∷ τ ∷ α ∷ ι ∷ []) "2Tim.2.13"
  ∷ word (Τ ∷ α ∷ ῦ ∷ τ ∷ α ∷ []) "2Tim.2.14"
  ∷ word (ὑ ∷ π ∷ ο ∷ μ ∷ ί ∷ μ ∷ ν ∷ ῃ ∷ σ ∷ κ ∷ ε ∷ []) "2Tim.2.14"
  ∷ word (δ ∷ ι ∷ α ∷ μ ∷ α ∷ ρ ∷ τ ∷ υ ∷ ρ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.2.14"
  ∷ word (ἐ ∷ ν ∷ ώ ∷ π ∷ ι ∷ ο ∷ ν ∷ []) "2Tim.2.14"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.2.14"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.2.14"
  ∷ word (μ ∷ ὴ ∷ []) "2Tim.2.14"
  ∷ word (∙λ ∷ ο ∷ γ ∷ ο ∷ μ ∷ α ∷ χ ∷ ε ∷ ῖ ∷ ν ∷ []) "2Tim.2.14"
  ∷ word (ἐ ∷ π ∷ []) "2Tim.2.14"
  ∷ word (ο ∷ ὐ ∷ δ ∷ ὲ ∷ ν ∷ []) "2Tim.2.14"
  ∷ word (χ ∷ ρ ∷ ή ∷ σ ∷ ι ∷ μ ∷ ο ∷ ν ∷ []) "2Tim.2.14"
  ∷ word (ἐ ∷ π ∷ ὶ ∷ []) "2Tim.2.14"
  ∷ word (κ ∷ α ∷ τ ∷ α ∷ σ ∷ τ ∷ ρ ∷ ο ∷ φ ∷ ῇ ∷ []) "2Tim.2.14"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "2Tim.2.14"
  ∷ word (ἀ ∷ κ ∷ ο ∷ υ ∷ ό ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "2Tim.2.14"
  ∷ word (σ ∷ π ∷ ο ∷ ύ ∷ δ ∷ α ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.2.15"
  ∷ word (σ ∷ ε ∷ α ∷ υ ∷ τ ∷ ὸ ∷ ν ∷ []) "2Tim.2.15"
  ∷ word (δ ∷ ό ∷ κ ∷ ι ∷ μ ∷ ο ∷ ν ∷ []) "2Tim.2.15"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ σ ∷ τ ∷ ῆ ∷ σ ∷ α ∷ ι ∷ []) "2Tim.2.15"
  ∷ word (τ ∷ ῷ ∷ []) "2Tim.2.15"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "2Tim.2.15"
  ∷ word (ἐ ∷ ρ ∷ γ ∷ ά ∷ τ ∷ η ∷ ν ∷ []) "2Tim.2.15"
  ∷ word (ἀ ∷ ν ∷ ε ∷ π ∷ α ∷ ί ∷ σ ∷ χ ∷ υ ∷ ν ∷ τ ∷ ο ∷ ν ∷ []) "2Tim.2.15"
  ∷ word (ὀ ∷ ρ ∷ θ ∷ ο ∷ τ ∷ ο ∷ μ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ α ∷ []) "2Tim.2.15"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.2.15"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ν ∷ []) "2Tim.2.15"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.2.15"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Tim.2.15"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2Tim.2.16"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.2.16"
  ∷ word (β ∷ ε ∷ β ∷ ή ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "2Tim.2.16"
  ∷ word (κ ∷ ε ∷ ν ∷ ο ∷ φ ∷ ω ∷ ν ∷ ί ∷ α ∷ ς ∷ []) "2Tim.2.16"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ ΐ ∷ σ ∷ τ ∷ α ∷ σ ∷ ο ∷ []) "2Tim.2.16"
  ∷ word (ἐ ∷ π ∷ ὶ ∷ []) "2Tim.2.16"
  ∷ word (π ∷ ∙λ ∷ ε ∷ ῖ ∷ ο ∷ ν ∷ []) "2Tim.2.16"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Tim.2.16"
  ∷ word (π ∷ ρ ∷ ο ∷ κ ∷ ό ∷ ψ ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.2.16"
  ∷ word (ἀ ∷ σ ∷ ε ∷ β ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Tim.2.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.17"
  ∷ word (ὁ ∷ []) "2Tim.2.17"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ς ∷ []) "2Tim.2.17"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῶ ∷ ν ∷ []) "2Tim.2.17"
  ∷ word (ὡ ∷ ς ∷ []) "2Tim.2.17"
  ∷ word (γ ∷ ά ∷ γ ∷ γ ∷ ρ ∷ α ∷ ι ∷ ν ∷ α ∷ []) "2Tim.2.17"
  ∷ word (ν ∷ ο ∷ μ ∷ ὴ ∷ ν ∷ []) "2Tim.2.17"
  ∷ word (ἕ ∷ ξ ∷ ε ∷ ι ∷ []) "2Tim.2.17"
  ∷ word (ὧ ∷ ν ∷ []) "2Tim.2.17"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.2.17"
  ∷ word (Ὑ ∷ μ ∷ έ ∷ ν ∷ α ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.2.17"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.17"
  ∷ word (Φ ∷ ί ∷ ∙λ ∷ η ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.2.17"
  ∷ word (ο ∷ ἵ ∷ τ ∷ ι ∷ ν ∷ ε ∷ ς ∷ []) "2Tim.2.18"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "2Tim.2.18"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.2.18"
  ∷ word (ἀ ∷ ∙λ ∷ ή ∷ θ ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "2Tim.2.18"
  ∷ word (ἠ ∷ σ ∷ τ ∷ ό ∷ χ ∷ η ∷ σ ∷ α ∷ ν ∷ []) "2Tim.2.18"
  ∷ word (∙λ ∷ έ ∷ γ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.2.18"
  ∷ word (ἀ ∷ ν ∷ ά ∷ σ ∷ τ ∷ α ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.2.18"
  ∷ word (ἤ ∷ δ ∷ η ∷ []) "2Tim.2.18"
  ∷ word (γ ∷ ε ∷ γ ∷ ο ∷ ν ∷ έ ∷ ν ∷ α ∷ ι ∷ []) "2Tim.2.18"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.18"
  ∷ word (ἀ ∷ ν ∷ α ∷ τ ∷ ρ ∷ έ ∷ π ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.2.18"
  ∷ word (τ ∷ ή ∷ ν ∷ []) "2Tim.2.18"
  ∷ word (τ ∷ ι ∷ ν ∷ ω ∷ ν ∷ []) "2Tim.2.18"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.2.18"
  ∷ word (ὁ ∷ []) "2Tim.2.19"
  ∷ word (μ ∷ έ ∷ ν ∷ τ ∷ ο ∷ ι ∷ []) "2Tim.2.19"
  ∷ word (σ ∷ τ ∷ ε ∷ ρ ∷ ε ∷ ὸ ∷ ς ∷ []) "2Tim.2.19"
  ∷ word (θ ∷ ε ∷ μ ∷ έ ∷ ∙λ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.2.19"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.2.19"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Tim.2.19"
  ∷ word (ἕ ∷ σ ∷ τ ∷ η ∷ κ ∷ ε ∷ ν ∷ []) "2Tim.2.19"
  ∷ word (ἔ ∷ χ ∷ ω ∷ ν ∷ []) "2Tim.2.19"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.2.19"
  ∷ word (σ ∷ φ ∷ ρ ∷ α ∷ γ ∷ ῖ ∷ δ ∷ α ∷ []) "2Tim.2.19"
  ∷ word (τ ∷ α ∷ ύ ∷ τ ∷ η ∷ ν ∷ []) "2Tim.2.19"
  ∷ word (Ἔ ∷ γ ∷ ν ∷ ω ∷ []) "2Tim.2.19"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.2.19"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Tim.2.19"
  ∷ word (ὄ ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "2Tim.2.19"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.2.19"
  ∷ word (κ ∷ α ∷ ί ∷ []) "2Tim.2.19"
  ∷ word (Ἀ ∷ π ∷ ο ∷ σ ∷ τ ∷ ή ∷ τ ∷ ω ∷ []) "2Tim.2.19"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Tim.2.19"
  ∷ word (ἀ ∷ δ ∷ ι ∷ κ ∷ ί ∷ α ∷ ς ∷ []) "2Tim.2.19"
  ∷ word (π ∷ ᾶ ∷ ς ∷ []) "2Tim.2.19"
  ∷ word (ὁ ∷ []) "2Tim.2.19"
  ∷ word (ὀ ∷ ν ∷ ο ∷ μ ∷ ά ∷ ζ ∷ ω ∷ ν ∷ []) "2Tim.2.19"
  ∷ word (τ ∷ ὸ ∷ []) "2Tim.2.19"
  ∷ word (ὄ ∷ ν ∷ ο ∷ μ ∷ α ∷ []) "2Tim.2.19"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.2.19"
  ∷ word (Ἐ ∷ ν ∷ []) "2Tim.2.20"
  ∷ word (μ ∷ ε ∷ γ ∷ ά ∷ ∙λ ∷ ῃ ∷ []) "2Tim.2.20"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.2.20"
  ∷ word (ο ∷ ἰ ∷ κ ∷ ί ∷ ᾳ ∷ []) "2Tim.2.20"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2Tim.2.20"
  ∷ word (ἔ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.2.20"
  ∷ word (μ ∷ ό ∷ ν ∷ ο ∷ ν ∷ []) "2Tim.2.20"
  ∷ word (σ ∷ κ ∷ ε ∷ ύ ∷ η ∷ []) "2Tim.2.20"
  ∷ word (χ ∷ ρ ∷ υ ∷ σ ∷ ᾶ ∷ []) "2Tim.2.20"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.20"
  ∷ word (ἀ ∷ ρ ∷ γ ∷ υ ∷ ρ ∷ ᾶ ∷ []) "2Tim.2.20"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.2.20"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.20"
  ∷ word (ξ ∷ ύ ∷ ∙λ ∷ ι ∷ ν ∷ α ∷ []) "2Tim.2.20"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.20"
  ∷ word (ὀ ∷ σ ∷ τ ∷ ρ ∷ ά ∷ κ ∷ ι ∷ ν ∷ α ∷ []) "2Tim.2.20"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.20"
  ∷ word (ἃ ∷ []) "2Tim.2.20"
  ∷ word (μ ∷ ὲ ∷ ν ∷ []) "2Tim.2.20"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.2.20"
  ∷ word (τ ∷ ι ∷ μ ∷ ὴ ∷ ν ∷ []) "2Tim.2.20"
  ∷ word (ἃ ∷ []) "2Tim.2.20"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.2.20"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.2.20"
  ∷ word (ἀ ∷ τ ∷ ι ∷ μ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.2.20"
  ∷ word (ἐ ∷ ὰ ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (ο ∷ ὖ ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (τ ∷ ι ∷ ς ∷ []) "2Tim.2.21"
  ∷ word (ἐ ∷ κ ∷ κ ∷ α ∷ θ ∷ ά ∷ ρ ∷ ῃ ∷ []) "2Tim.2.21"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ὸ ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Tim.2.21"
  ∷ word (τ ∷ ο ∷ ύ ∷ τ ∷ ω ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (ἔ ∷ σ ∷ τ ∷ α ∷ ι ∷ []) "2Tim.2.21"
  ∷ word (σ ∷ κ ∷ ε ∷ ῦ ∷ ο ∷ ς ∷ []) "2Tim.2.21"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.2.21"
  ∷ word (τ ∷ ι ∷ μ ∷ ή ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (ἡ ∷ γ ∷ ι ∷ α ∷ σ ∷ μ ∷ έ ∷ ν ∷ ο ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (ε ∷ ὔ ∷ χ ∷ ρ ∷ η ∷ σ ∷ τ ∷ ο ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (τ ∷ ῷ ∷ []) "2Tim.2.21"
  ∷ word (δ ∷ ε ∷ σ ∷ π ∷ ό ∷ τ ∷ ῃ ∷ []) "2Tim.2.21"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.2.21"
  ∷ word (π ∷ ᾶ ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ο ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ὸ ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (ἡ ∷ τ ∷ ο ∷ ι ∷ μ ∷ α ∷ σ ∷ μ ∷ έ ∷ ν ∷ ο ∷ ν ∷ []) "2Tim.2.21"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2Tim.2.22"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.2.22"
  ∷ word (ν ∷ ε ∷ ω ∷ τ ∷ ε ∷ ρ ∷ ι ∷ κ ∷ ὰ ∷ ς ∷ []) "2Tim.2.22"
  ∷ word (ἐ ∷ π ∷ ι ∷ θ ∷ υ ∷ μ ∷ ί ∷ α ∷ ς ∷ []) "2Tim.2.22"
  ∷ word (φ ∷ ε ∷ ῦ ∷ γ ∷ ε ∷ []) "2Tim.2.22"
  ∷ word (δ ∷ ί ∷ ω ∷ κ ∷ ε ∷ []) "2Tim.2.22"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.2.22"
  ∷ word (δ ∷ ι ∷ κ ∷ α ∷ ι ∷ ο ∷ σ ∷ ύ ∷ ν ∷ η ∷ ν ∷ []) "2Tim.2.22"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.2.22"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ η ∷ ν ∷ []) "2Tim.2.22"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ ν ∷ []) "2Tim.2.22"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "2Tim.2.22"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "2Tim.2.22"
  ∷ word (ἐ ∷ π ∷ ι ∷ κ ∷ α ∷ ∙λ ∷ ο ∷ υ ∷ μ ∷ έ ∷ ν ∷ ω ∷ ν ∷ []) "2Tim.2.22"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.2.22"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ν ∷ []) "2Tim.2.22"
  ∷ word (ἐ ∷ κ ∷ []) "2Tim.2.22"
  ∷ word (κ ∷ α ∷ θ ∷ α ∷ ρ ∷ ᾶ ∷ ς ∷ []) "2Tim.2.22"
  ∷ word (κ ∷ α ∷ ρ ∷ δ ∷ ί ∷ α ∷ ς ∷ []) "2Tim.2.22"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2Tim.2.23"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.2.23"
  ∷ word (μ ∷ ω ∷ ρ ∷ ὰ ∷ ς ∷ []) "2Tim.2.23"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.23"
  ∷ word (ἀ ∷ π ∷ α ∷ ι ∷ δ ∷ ε ∷ ύ ∷ τ ∷ ο ∷ υ ∷ ς ∷ []) "2Tim.2.23"
  ∷ word (ζ ∷ η ∷ τ ∷ ή ∷ σ ∷ ε ∷ ι ∷ ς ∷ []) "2Tim.2.23"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ ι ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.2.23"
  ∷ word (ε ∷ ἰ ∷ δ ∷ ὼ ∷ ς ∷ []) "2Tim.2.23"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Tim.2.23"
  ∷ word (γ ∷ ε ∷ ν ∷ ν ∷ ῶ ∷ σ ∷ ι ∷ []) "2Tim.2.23"
  ∷ word (μ ∷ ά ∷ χ ∷ α ∷ ς ∷ []) "2Tim.2.23"
  ∷ word (δ ∷ ο ∷ ῦ ∷ ∙λ ∷ ο ∷ ν ∷ []) "2Tim.2.24"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.2.24"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Tim.2.24"
  ∷ word (ο ∷ ὐ ∷ []) "2Tim.2.24"
  ∷ word (δ ∷ ε ∷ ῖ ∷ []) "2Tim.2.24"
  ∷ word (μ ∷ ά ∷ χ ∷ ε ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2Tim.2.24"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.2.24"
  ∷ word (ἤ ∷ π ∷ ι ∷ ο ∷ ν ∷ []) "2Tim.2.24"
  ∷ word (ε ∷ ἶ ∷ ν ∷ α ∷ ι ∷ []) "2Tim.2.24"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Tim.2.24"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "2Tim.2.24"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ κ ∷ τ ∷ ι ∷ κ ∷ ό ∷ ν ∷ []) "2Tim.2.24"
  ∷ word (ἀ ∷ ν ∷ ε ∷ ξ ∷ ί ∷ κ ∷ α ∷ κ ∷ ο ∷ ν ∷ []) "2Tim.2.24"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.2.25"
  ∷ word (π ∷ ρ ∷ α ∷ ΰ ∷ τ ∷ η ∷ τ ∷ ι ∷ []) "2Tim.2.25"
  ∷ word (π ∷ α ∷ ι ∷ δ ∷ ε ∷ ύ ∷ ο ∷ ν ∷ τ ∷ α ∷ []) "2Tim.2.25"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Tim.2.25"
  ∷ word (ἀ ∷ ν ∷ τ ∷ ι ∷ δ ∷ ι ∷ α ∷ τ ∷ ι ∷ θ ∷ ε ∷ μ ∷ έ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "2Tim.2.25"
  ∷ word (μ ∷ ή ∷ π ∷ ο ∷ τ ∷ ε ∷ []) "2Tim.2.25"
  ∷ word (δ ∷ ώ ∷ ῃ ∷ []) "2Tim.2.25"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Tim.2.25"
  ∷ word (ὁ ∷ []) "2Tim.2.25"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ς ∷ []) "2Tim.2.25"
  ∷ word (μ ∷ ε ∷ τ ∷ ά ∷ ν ∷ ο ∷ ι ∷ α ∷ ν ∷ []) "2Tim.2.25"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.2.25"
  ∷ word (ἐ ∷ π ∷ ί ∷ γ ∷ ν ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.2.25"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Tim.2.25"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.2.26"
  ∷ word (ἀ ∷ ν ∷ α ∷ ν ∷ ή ∷ ψ ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.2.26"
  ∷ word (ἐ ∷ κ ∷ []) "2Tim.2.26"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.2.26"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.2.26"
  ∷ word (δ ∷ ι ∷ α ∷ β ∷ ό ∷ ∙λ ∷ ο ∷ υ ∷ []) "2Tim.2.26"
  ∷ word (π ∷ α ∷ γ ∷ ί ∷ δ ∷ ο ∷ ς ∷ []) "2Tim.2.26"
  ∷ word (ἐ ∷ ζ ∷ ω ∷ γ ∷ ρ ∷ η ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ []) "2Tim.2.26"
  ∷ word (ὑ ∷ π ∷ []) "2Tim.2.26"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.2.26"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.2.26"
  ∷ word (τ ∷ ὸ ∷ []) "2Tim.2.26"
  ∷ word (ἐ ∷ κ ∷ ε ∷ ί ∷ ν ∷ ο ∷ υ ∷ []) "2Tim.2.26"
  ∷ word (θ ∷ έ ∷ ∙λ ∷ η ∷ μ ∷ α ∷ []) "2Tim.2.26"
  ∷ word (Τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "2Tim.3.1"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.3.1"
  ∷ word (γ ∷ ί ∷ ν ∷ ω ∷ σ ∷ κ ∷ ε ∷ []) "2Tim.3.1"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Tim.3.1"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.3.1"
  ∷ word (ἐ ∷ σ ∷ χ ∷ ά ∷ τ ∷ α ∷ ι ∷ ς ∷ []) "2Tim.3.1"
  ∷ word (ἡ ∷ μ ∷ έ ∷ ρ ∷ α ∷ ι ∷ ς ∷ []) "2Tim.3.1"
  ∷ word (ἐ ∷ ν ∷ σ ∷ τ ∷ ή ∷ σ ∷ ο ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "2Tim.3.1"
  ∷ word (κ ∷ α ∷ ι ∷ ρ ∷ ο ∷ ὶ ∷ []) "2Tim.3.1"
  ∷ word (χ ∷ α ∷ ∙λ ∷ ε ∷ π ∷ ο ∷ ί ∷ []) "2Tim.3.1"
  ∷ word (ἔ ∷ σ ∷ ο ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "2Tim.3.2"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Tim.3.2"
  ∷ word (ο ∷ ἱ ∷ []) "2Tim.3.2"
  ∷ word (ἄ ∷ ν ∷ θ ∷ ρ ∷ ω ∷ π ∷ ο ∷ ι ∷ []) "2Tim.3.2"
  ∷ word (φ ∷ ί ∷ ∙λ ∷ α ∷ υ ∷ τ ∷ ο ∷ ι ∷ []) "2Tim.3.2"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ ά ∷ ρ ∷ γ ∷ υ ∷ ρ ∷ ο ∷ ι ∷ []) "2Tim.3.2"
  ∷ word (ἀ ∷ ∙λ ∷ α ∷ ζ ∷ ό ∷ ν ∷ ε ∷ ς ∷ []) "2Tim.3.2"
  ∷ word (ὑ ∷ π ∷ ε ∷ ρ ∷ ή ∷ φ ∷ α ∷ ν ∷ ο ∷ ι ∷ []) "2Tim.3.2"
  ∷ word (β ∷ ∙λ ∷ ά ∷ σ ∷ φ ∷ η ∷ μ ∷ ο ∷ ι ∷ []) "2Tim.3.2"
  ∷ word (γ ∷ ο ∷ ν ∷ ε ∷ ῦ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.3.2"
  ∷ word (ἀ ∷ π ∷ ε ∷ ι ∷ θ ∷ ε ∷ ῖ ∷ ς ∷ []) "2Tim.3.2"
  ∷ word (ἀ ∷ χ ∷ ά ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ι ∷ []) "2Tim.3.2"
  ∷ word (ἀ ∷ ν ∷ ό ∷ σ ∷ ι ∷ ο ∷ ι ∷ []) "2Tim.3.2"
  ∷ word (ἄ ∷ σ ∷ τ ∷ ο ∷ ρ ∷ γ ∷ ο ∷ ι ∷ []) "2Tim.3.3"
  ∷ word (ἄ ∷ σ ∷ π ∷ ο ∷ ν ∷ δ ∷ ο ∷ ι ∷ []) "2Tim.3.3"
  ∷ word (δ ∷ ι ∷ ά ∷ β ∷ ο ∷ ∙λ ∷ ο ∷ ι ∷ []) "2Tim.3.3"
  ∷ word (ἀ ∷ κ ∷ ρ ∷ α ∷ τ ∷ ε ∷ ῖ ∷ ς ∷ []) "2Tim.3.3"
  ∷ word (ἀ ∷ ν ∷ ή ∷ μ ∷ ε ∷ ρ ∷ ο ∷ ι ∷ []) "2Tim.3.3"
  ∷ word (ἀ ∷ φ ∷ ι ∷ ∙λ ∷ ά ∷ γ ∷ α ∷ θ ∷ ο ∷ ι ∷ []) "2Tim.3.3"
  ∷ word (π ∷ ρ ∷ ο ∷ δ ∷ ό ∷ τ ∷ α ∷ ι ∷ []) "2Tim.3.4"
  ∷ word (π ∷ ρ ∷ ο ∷ π ∷ ε ∷ τ ∷ ε ∷ ῖ ∷ ς ∷ []) "2Tim.3.4"
  ∷ word (τ ∷ ε ∷ τ ∷ υ ∷ φ ∷ ω ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ []) "2Tim.3.4"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ ή ∷ δ ∷ ο ∷ ν ∷ ο ∷ ι ∷ []) "2Tim.3.4"
  ∷ word (μ ∷ ᾶ ∷ ∙λ ∷ ∙λ ∷ ο ∷ ν ∷ []) "2Tim.3.4"
  ∷ word (ἢ ∷ []) "2Tim.3.4"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ ό ∷ θ ∷ ε ∷ ο ∷ ι ∷ []) "2Tim.3.4"
  ∷ word (ἔ ∷ χ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.3.5"
  ∷ word (μ ∷ ό ∷ ρ ∷ φ ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.3.5"
  ∷ word (ε ∷ ὐ ∷ σ ∷ ε ∷ β ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Tim.3.5"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.3.5"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.3.5"
  ∷ word (δ ∷ ύ ∷ ν ∷ α ∷ μ ∷ ι ∷ ν ∷ []) "2Tim.3.5"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῆ ∷ ς ∷ []) "2Tim.3.5"
  ∷ word (ἠ ∷ ρ ∷ ν ∷ η ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ []) "2Tim.3.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.5"
  ∷ word (τ ∷ ο ∷ ύ ∷ τ ∷ ο ∷ υ ∷ ς ∷ []) "2Tim.3.5"
  ∷ word (ἀ ∷ π ∷ ο ∷ τ ∷ ρ ∷ έ ∷ π ∷ ο ∷ υ ∷ []) "2Tim.3.5"
  ∷ word (ἐ ∷ κ ∷ []) "2Tim.3.6"
  ∷ word (τ ∷ ο ∷ ύ ∷ τ ∷ ω ∷ ν ∷ []) "2Tim.3.6"
  ∷ word (γ ∷ ά ∷ ρ ∷ []) "2Tim.3.6"
  ∷ word (ε ∷ ἰ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.3.6"
  ∷ word (ο ∷ ἱ ∷ []) "2Tim.3.6"
  ∷ word (ἐ ∷ ν ∷ δ ∷ ύ ∷ ν ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.3.6"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.3.6"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2Tim.3.6"
  ∷ word (ο ∷ ἰ ∷ κ ∷ ί ∷ α ∷ ς ∷ []) "2Tim.3.6"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.6"
  ∷ word (α ∷ ἰ ∷ χ ∷ μ ∷ α ∷ ∙λ ∷ ω ∷ τ ∷ ί ∷ ζ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.3.6"
  ∷ word (γ ∷ υ ∷ ν ∷ α ∷ ι ∷ κ ∷ ά ∷ ρ ∷ ι ∷ α ∷ []) "2Tim.3.6"
  ∷ word (σ ∷ ε ∷ σ ∷ ω ∷ ρ ∷ ε ∷ υ ∷ μ ∷ έ ∷ ν ∷ α ∷ []) "2Tim.3.6"
  ∷ word (ἁ ∷ μ ∷ α ∷ ρ ∷ τ ∷ ί ∷ α ∷ ι ∷ ς ∷ []) "2Tim.3.6"
  ∷ word (ἀ ∷ γ ∷ ό ∷ μ ∷ ε ∷ ν ∷ α ∷ []) "2Tim.3.6"
  ∷ word (ἐ ∷ π ∷ ι ∷ θ ∷ υ ∷ μ ∷ ί ∷ α ∷ ι ∷ ς ∷ []) "2Tim.3.6"
  ∷ word (π ∷ ο ∷ ι ∷ κ ∷ ί ∷ ∙λ ∷ α ∷ ι ∷ ς ∷ []) "2Tim.3.6"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ο ∷ τ ∷ ε ∷ []) "2Tim.3.7"
  ∷ word (μ ∷ α ∷ ν ∷ θ ∷ ά ∷ ν ∷ ο ∷ ν ∷ τ ∷ α ∷ []) "2Tim.3.7"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.7"
  ∷ word (μ ∷ η ∷ δ ∷ έ ∷ π ∷ ο ∷ τ ∷ ε ∷ []) "2Tim.3.7"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.3.7"
  ∷ word (ἐ ∷ π ∷ ί ∷ γ ∷ ν ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.3.7"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Tim.3.7"
  ∷ word (ἐ ∷ ∙λ ∷ θ ∷ ε ∷ ῖ ∷ ν ∷ []) "2Tim.3.7"
  ∷ word (δ ∷ υ ∷ ν ∷ ά ∷ μ ∷ ε ∷ ν ∷ α ∷ []) "2Tim.3.7"
  ∷ word (ὃ ∷ ν ∷ []) "2Tim.3.8"
  ∷ word (τ ∷ ρ ∷ ό ∷ π ∷ ο ∷ ν ∷ []) "2Tim.3.8"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.3.8"
  ∷ word (Ἰ ∷ ά ∷ ν ∷ ν ∷ η ∷ ς ∷ []) "2Tim.3.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.8"
  ∷ word (Ἰ ∷ α ∷ μ ∷ β ∷ ρ ∷ ῆ ∷ ς ∷ []) "2Tim.3.8"
  ∷ word (ἀ ∷ ν ∷ τ ∷ έ ∷ σ ∷ τ ∷ η ∷ σ ∷ α ∷ ν ∷ []) "2Tim.3.8"
  ∷ word (Μ ∷ ω ∷ ϋ ∷ σ ∷ ε ∷ ῖ ∷ []) "2Tim.3.8"
  ∷ word (ο ∷ ὕ ∷ τ ∷ ω ∷ ς ∷ []) "2Tim.3.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.8"
  ∷ word (ο ∷ ὗ ∷ τ ∷ ο ∷ ι ∷ []) "2Tim.3.8"
  ∷ word (ἀ ∷ ν ∷ θ ∷ ί ∷ σ ∷ τ ∷ α ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "2Tim.3.8"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.3.8"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "2Tim.3.8"
  ∷ word (ἄ ∷ ν ∷ θ ∷ ρ ∷ ω ∷ π ∷ ο ∷ ι ∷ []) "2Tim.3.8"
  ∷ word (κ ∷ α ∷ τ ∷ ε ∷ φ ∷ θ ∷ α ∷ ρ ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ []) "2Tim.3.8"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.3.8"
  ∷ word (ν ∷ ο ∷ ῦ ∷ ν ∷ []) "2Tim.3.8"
  ∷ word (ἀ ∷ δ ∷ ό ∷ κ ∷ ι ∷ μ ∷ ο ∷ ι ∷ []) "2Tim.3.8"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "2Tim.3.8"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.3.8"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.3.8"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ []) "2Tim.3.9"
  ∷ word (ο ∷ ὐ ∷ []) "2Tim.3.9"
  ∷ word (π ∷ ρ ∷ ο ∷ κ ∷ ό ∷ ψ ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.3.9"
  ∷ word (ἐ ∷ π ∷ ὶ ∷ []) "2Tim.3.9"
  ∷ word (π ∷ ∙λ ∷ ε ∷ ῖ ∷ ο ∷ ν ∷ []) "2Tim.3.9"
  ∷ word (ἡ ∷ []) "2Tim.3.9"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Tim.3.9"
  ∷ word (ἄ ∷ ν ∷ ο ∷ ι ∷ α ∷ []) "2Tim.3.9"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῶ ∷ ν ∷ []) "2Tim.3.9"
  ∷ word (ἔ ∷ κ ∷ δ ∷ η ∷ ∙λ ∷ ο ∷ ς ∷ []) "2Tim.3.9"
  ∷ word (ἔ ∷ σ ∷ τ ∷ α ∷ ι ∷ []) "2Tim.3.9"
  ∷ word (π ∷ ᾶ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.3.9"
  ∷ word (ὡ ∷ ς ∷ []) "2Tim.3.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.9"
  ∷ word (ἡ ∷ []) "2Tim.3.9"
  ∷ word (ἐ ∷ κ ∷ ε ∷ ί ∷ ν ∷ ω ∷ ν ∷ []) "2Tim.3.9"
  ∷ word (ἐ ∷ γ ∷ έ ∷ ν ∷ ε ∷ τ ∷ ο ∷ []) "2Tim.3.9"
  ∷ word (Σ ∷ ὺ ∷ []) "2Tim.3.10"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.3.10"
  ∷ word (π ∷ α ∷ ρ ∷ η ∷ κ ∷ ο ∷ ∙λ ∷ ο ∷ ύ ∷ θ ∷ η ∷ σ ∷ ά ∷ ς ∷ []) "2Tim.3.10"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "2Tim.3.10"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.3.10"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ σ ∷ κ ∷ α ∷ ∙λ ∷ ί ∷ ᾳ ∷ []) "2Tim.3.10"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.3.10"
  ∷ word (ἀ ∷ γ ∷ ω ∷ γ ∷ ῇ ∷ []) "2Tim.3.10"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.3.10"
  ∷ word (π ∷ ρ ∷ ο ∷ θ ∷ έ ∷ σ ∷ ε ∷ ι ∷ []) "2Tim.3.10"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.3.10"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ι ∷ []) "2Tim.3.10"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.3.10"
  ∷ word (μ ∷ α ∷ κ ∷ ρ ∷ ο ∷ θ ∷ υ ∷ μ ∷ ί ∷ ᾳ ∷ []) "2Tim.3.10"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.3.10"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ ῃ ∷ []) "2Tim.3.10"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.3.10"
  ∷ word (ὑ ∷ π ∷ ο ∷ μ ∷ ο ∷ ν ∷ ῇ ∷ []) "2Tim.3.10"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Tim.3.11"
  ∷ word (δ ∷ ι ∷ ω ∷ γ ∷ μ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Tim.3.11"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Tim.3.11"
  ∷ word (π ∷ α ∷ θ ∷ ή ∷ μ ∷ α ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.3.11"
  ∷ word (ο ∷ ἷ ∷ ά ∷ []) "2Tim.3.11"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "2Tim.3.11"
  ∷ word (ἐ ∷ γ ∷ έ ∷ ν ∷ ε ∷ τ ∷ ο ∷ []) "2Tim.3.11"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.3.11"
  ∷ word (Ἀ ∷ ν ∷ τ ∷ ι ∷ ο ∷ χ ∷ ε ∷ ί ∷ ᾳ ∷ []) "2Tim.3.11"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.3.11"
  ∷ word (Ἰ ∷ κ ∷ ο ∷ ν ∷ ί ∷ ῳ ∷ []) "2Tim.3.11"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.3.11"
  ∷ word (Λ ∷ ύ ∷ σ ∷ τ ∷ ρ ∷ ο ∷ ι ∷ ς ∷ []) "2Tim.3.11"
  ∷ word (ο ∷ ἵ ∷ ο ∷ υ ∷ ς ∷ []) "2Tim.3.11"
  ∷ word (δ ∷ ι ∷ ω ∷ γ ∷ μ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Tim.3.11"
  ∷ word (ὑ ∷ π ∷ ή ∷ ν ∷ ε ∷ γ ∷ κ ∷ α ∷ []) "2Tim.3.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.11"
  ∷ word (ἐ ∷ κ ∷ []) "2Tim.3.11"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "2Tim.3.11"
  ∷ word (μ ∷ ε ∷ []) "2Tim.3.11"
  ∷ word (ἐ ∷ ρ ∷ ρ ∷ ύ ∷ σ ∷ α ∷ τ ∷ ο ∷ []) "2Tim.3.11"
  ∷ word (ὁ ∷ []) "2Tim.3.11"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.3.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.12"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.3.12"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.3.12"
  ∷ word (ο ∷ ἱ ∷ []) "2Tim.3.12"
  ∷ word (θ ∷ έ ∷ ∙λ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.3.12"
  ∷ word (ζ ∷ ῆ ∷ ν ∷ []) "2Tim.3.12"
  ∷ word (ε ∷ ὐ ∷ σ ∷ ε ∷ β ∷ ῶ ∷ ς ∷ []) "2Tim.3.12"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.3.12"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "2Tim.3.12"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.3.12"
  ∷ word (δ ∷ ι ∷ ω ∷ χ ∷ θ ∷ ή ∷ σ ∷ ο ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "2Tim.3.12"
  ∷ word (π ∷ ο ∷ ν ∷ η ∷ ρ ∷ ο ∷ ὶ ∷ []) "2Tim.3.13"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.3.13"
  ∷ word (ἄ ∷ ν ∷ θ ∷ ρ ∷ ω ∷ π ∷ ο ∷ ι ∷ []) "2Tim.3.13"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.13"
  ∷ word (γ ∷ ό ∷ η ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.3.13"
  ∷ word (π ∷ ρ ∷ ο ∷ κ ∷ ό ∷ ψ ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.3.13"
  ∷ word (ἐ ∷ π ∷ ὶ ∷ []) "2Tim.3.13"
  ∷ word (τ ∷ ὸ ∷ []) "2Tim.3.13"
  ∷ word (χ ∷ ε ∷ ῖ ∷ ρ ∷ ο ∷ ν ∷ []) "2Tim.3.13"
  ∷ word (π ∷ ∙λ ∷ α ∷ ν ∷ ῶ ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.3.13"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.13"
  ∷ word (π ∷ ∙λ ∷ α ∷ ν ∷ ώ ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "2Tim.3.13"
  ∷ word (σ ∷ ὺ ∷ []) "2Tim.3.14"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.3.14"
  ∷ word (μ ∷ έ ∷ ν ∷ ε ∷ []) "2Tim.3.14"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.3.14"
  ∷ word (ο ∷ ἷ ∷ ς ∷ []) "2Tim.3.14"
  ∷ word (ἔ ∷ μ ∷ α ∷ θ ∷ ε ∷ ς ∷ []) "2Tim.3.14"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.14"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ τ ∷ ώ ∷ θ ∷ η ∷ ς ∷ []) "2Tim.3.14"
  ∷ word (ε ∷ ἰ ∷ δ ∷ ὼ ∷ ς ∷ []) "2Tim.3.14"
  ∷ word (π ∷ α ∷ ρ ∷ ὰ ∷ []) "2Tim.3.14"
  ∷ word (τ ∷ ί ∷ ν ∷ ω ∷ ν ∷ []) "2Tim.3.14"
  ∷ word (ἔ ∷ μ ∷ α ∷ θ ∷ ε ∷ ς ∷ []) "2Tim.3.14"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.15"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Tim.3.15"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Tim.3.15"
  ∷ word (β ∷ ρ ∷ έ ∷ φ ∷ ο ∷ υ ∷ ς ∷ []) "2Tim.3.15"
  ∷ word (ἱ ∷ ε ∷ ρ ∷ ὰ ∷ []) "2Tim.3.15"
  ∷ word (γ ∷ ρ ∷ ά ∷ μ ∷ μ ∷ α ∷ τ ∷ α ∷ []) "2Tim.3.15"
  ∷ word (ο ∷ ἶ ∷ δ ∷ α ∷ ς ∷ []) "2Tim.3.15"
  ∷ word (τ ∷ ὰ ∷ []) "2Tim.3.15"
  ∷ word (δ ∷ υ ∷ ν ∷ ά ∷ μ ∷ ε ∷ ν ∷ ά ∷ []) "2Tim.3.15"
  ∷ word (σ ∷ ε ∷ []) "2Tim.3.15"
  ∷ word (σ ∷ ο ∷ φ ∷ ί ∷ σ ∷ α ∷ ι ∷ []) "2Tim.3.15"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.3.15"
  ∷ word (σ ∷ ω ∷ τ ∷ η ∷ ρ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.3.15"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Tim.3.15"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ω ∷ ς ∷ []) "2Tim.3.15"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.3.15"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.3.15"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "2Tim.3.15"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.3.15"
  ∷ word (π ∷ ᾶ ∷ σ ∷ α ∷ []) "2Tim.3.16"
  ∷ word (γ ∷ ρ ∷ α ∷ φ ∷ ὴ ∷ []) "2Tim.3.16"
  ∷ word (θ ∷ ε ∷ ό ∷ π ∷ ν ∷ ε ∷ υ ∷ σ ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.3.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.3.16"
  ∷ word (ὠ ∷ φ ∷ έ ∷ ∙λ ∷ ι ∷ μ ∷ ο ∷ ς ∷ []) "2Tim.3.16"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Tim.3.16"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ σ ∷ κ ∷ α ∷ ∙λ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.3.16"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Tim.3.16"
  ∷ word (ἐ ∷ ∙λ ∷ ε ∷ γ ∷ μ ∷ ό ∷ ν ∷ []) "2Tim.3.16"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Tim.3.16"
  ∷ word (ἐ ∷ π ∷ α ∷ ν ∷ ό ∷ ρ ∷ θ ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.3.16"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Tim.3.16"
  ∷ word (π ∷ α ∷ ι ∷ δ ∷ ε ∷ ί ∷ α ∷ ν ∷ []) "2Tim.3.16"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.3.16"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.3.16"
  ∷ word (δ ∷ ι ∷ κ ∷ α ∷ ι ∷ ο ∷ σ ∷ ύ ∷ ν ∷ ῃ ∷ []) "2Tim.3.16"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Tim.3.17"
  ∷ word (ἄ ∷ ρ ∷ τ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.3.17"
  ∷ word (ᾖ ∷ []) "2Tim.3.17"
  ∷ word (ὁ ∷ []) "2Tim.3.17"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.3.17"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Tim.3.17"
  ∷ word (ἄ ∷ ν ∷ θ ∷ ρ ∷ ω ∷ π ∷ ο ∷ ς ∷ []) "2Tim.3.17"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Tim.3.17"
  ∷ word (π ∷ ᾶ ∷ ν ∷ []) "2Tim.3.17"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ο ∷ ν ∷ []) "2Tim.3.17"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ὸ ∷ ν ∷ []) "2Tim.3.17"
  ∷ word (ἐ ∷ ξ ∷ η ∷ ρ ∷ τ ∷ ι ∷ σ ∷ μ ∷ έ ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.3.17"
  ∷ word (Δ ∷ ι ∷ α ∷ μ ∷ α ∷ ρ ∷ τ ∷ ύ ∷ ρ ∷ ο ∷ μ ∷ α ∷ ι ∷ []) "2Tim.4.1"
  ∷ word (ἐ ∷ ν ∷ ώ ∷ π ∷ ι ∷ ο ∷ ν ∷ []) "2Tim.4.1"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.1"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Tim.4.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Tim.4.1"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.1"
  ∷ word (μ ∷ έ ∷ ∙λ ∷ ∙λ ∷ ο ∷ ν ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.4.1"
  ∷ word (κ ∷ ρ ∷ ί ∷ ν ∷ ε ∷ ι ∷ ν ∷ []) "2Tim.4.1"
  ∷ word (ζ ∷ ῶ ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "2Tim.4.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.1"
  ∷ word (ν ∷ ε ∷ κ ∷ ρ ∷ ο ∷ ύ ∷ ς ∷ []) "2Tim.4.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.1"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.4.1"
  ∷ word (ἐ ∷ π ∷ ι ∷ φ ∷ ά ∷ ν ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "2Tim.4.1"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.1"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.4.1"
  ∷ word (β ∷ α ∷ σ ∷ ι ∷ ∙λ ∷ ε ∷ ί ∷ α ∷ ν ∷ []) "2Tim.4.1"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.1"
  ∷ word (κ ∷ ή ∷ ρ ∷ υ ∷ ξ ∷ ο ∷ ν ∷ []) "2Tim.4.2"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.4.2"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ν ∷ []) "2Tim.4.2"
  ∷ word (ἐ ∷ π ∷ ί ∷ σ ∷ τ ∷ η ∷ θ ∷ ι ∷ []) "2Tim.4.2"
  ∷ word (ε ∷ ὐ ∷ κ ∷ α ∷ ί ∷ ρ ∷ ω ∷ ς ∷ []) "2Tim.4.2"
  ∷ word (ἀ ∷ κ ∷ α ∷ ί ∷ ρ ∷ ω ∷ ς ∷ []) "2Tim.4.2"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ γ ∷ ξ ∷ ο ∷ ν ∷ []) "2Tim.4.2"
  ∷ word (ἐ ∷ π ∷ ι ∷ τ ∷ ί ∷ μ ∷ η ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.4.2"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ κ ∷ ά ∷ ∙λ ∷ ε ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.4.2"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.4.2"
  ∷ word (π ∷ ά ∷ σ ∷ ῃ ∷ []) "2Tim.4.2"
  ∷ word (μ ∷ α ∷ κ ∷ ρ ∷ ο ∷ θ ∷ υ ∷ μ ∷ ί ∷ ᾳ ∷ []) "2Tim.4.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.2"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ χ ∷ ῇ ∷ []) "2Tim.4.2"
  ∷ word (ἔ ∷ σ ∷ τ ∷ α ∷ ι ∷ []) "2Tim.4.3"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Tim.4.3"
  ∷ word (κ ∷ α ∷ ι ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Tim.4.3"
  ∷ word (ὅ ∷ τ ∷ ε ∷ []) "2Tim.4.3"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.4.3"
  ∷ word (ὑ ∷ γ ∷ ι ∷ α ∷ ι ∷ ν ∷ ο ∷ ύ ∷ σ ∷ η ∷ ς ∷ []) "2Tim.4.3"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ σ ∷ κ ∷ α ∷ ∙λ ∷ ί ∷ α ∷ ς ∷ []) "2Tim.4.3"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2Tim.4.3"
  ∷ word (ἀ ∷ ν ∷ έ ∷ ξ ∷ ο ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "2Tim.4.3"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.4.3"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2Tim.4.3"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2Tim.4.3"
  ∷ word (ἰ ∷ δ ∷ ί ∷ α ∷ ς ∷ []) "2Tim.4.3"
  ∷ word (ἐ ∷ π ∷ ι ∷ θ ∷ υ ∷ μ ∷ ί ∷ α ∷ ς ∷ []) "2Tim.4.3"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Tim.4.3"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ ω ∷ ρ ∷ ε ∷ ύ ∷ σ ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.4.3"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ σ ∷ κ ∷ ά ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "2Tim.4.3"
  ∷ word (κ ∷ ν ∷ η ∷ θ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "2Tim.4.3"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.4.3"
  ∷ word (ἀ ∷ κ ∷ ο ∷ ή ∷ ν ∷ []) "2Tim.4.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.4"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Tim.4.4"
  ∷ word (μ ∷ ὲ ∷ ν ∷ []) "2Tim.4.4"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.4.4"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Tim.4.4"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.4.4"
  ∷ word (ἀ ∷ κ ∷ ο ∷ ὴ ∷ ν ∷ []) "2Tim.4.4"
  ∷ word (ἀ ∷ π ∷ ο ∷ σ ∷ τ ∷ ρ ∷ έ ∷ ψ ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.4.4"
  ∷ word (ἐ ∷ π ∷ ὶ ∷ []) "2Tim.4.4"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.4.4"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Tim.4.4"
  ∷ word (μ ∷ ύ ∷ θ ∷ ο ∷ υ ∷ ς ∷ []) "2Tim.4.4"
  ∷ word (ἐ ∷ κ ∷ τ ∷ ρ ∷ α ∷ π ∷ ή ∷ σ ∷ ο ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "2Tim.4.4"
  ∷ word (σ ∷ ὺ ∷ []) "2Tim.4.5"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.4.5"
  ∷ word (ν ∷ ῆ ∷ φ ∷ ε ∷ []) "2Tim.4.5"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.4.5"
  ∷ word (π ∷ ᾶ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.4.5"
  ∷ word (κ ∷ α ∷ κ ∷ ο ∷ π ∷ ά ∷ θ ∷ η ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.4.5"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ο ∷ ν ∷ []) "2Tim.4.5"
  ∷ word (π ∷ ο ∷ ί ∷ η ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.4.5"
  ∷ word (ε ∷ ὐ ∷ α ∷ γ ∷ γ ∷ ε ∷ ∙λ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.5"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.4.5"
  ∷ word (δ ∷ ι ∷ α ∷ κ ∷ ο ∷ ν ∷ ί ∷ α ∷ ν ∷ []) "2Tim.4.5"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "2Tim.4.5"
  ∷ word (π ∷ ∙λ ∷ η ∷ ρ ∷ ο ∷ φ ∷ ό ∷ ρ ∷ η ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.4.5"
  ∷ word (Ἐ ∷ γ ∷ ὼ ∷ []) "2Tim.4.6"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Tim.4.6"
  ∷ word (ἤ ∷ δ ∷ η ∷ []) "2Tim.4.6"
  ∷ word (σ ∷ π ∷ έ ∷ ν ∷ δ ∷ ο ∷ μ ∷ α ∷ ι ∷ []) "2Tim.4.6"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.6"
  ∷ word (ὁ ∷ []) "2Tim.4.6"
  ∷ word (κ ∷ α ∷ ι ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Tim.4.6"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.4.6"
  ∷ word (ἀ ∷ ν ∷ α ∷ ∙λ ∷ ύ ∷ σ ∷ ε ∷ ώ ∷ ς ∷ []) "2Tim.4.6"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "2Tim.4.6"
  ∷ word (ἐ ∷ φ ∷ έ ∷ σ ∷ τ ∷ η ∷ κ ∷ ε ∷ ν ∷ []) "2Tim.4.6"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.4.7"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ὸ ∷ ν ∷ []) "2Tim.4.7"
  ∷ word (ἀ ∷ γ ∷ ῶ ∷ ν ∷ α ∷ []) "2Tim.4.7"
  ∷ word (ἠ ∷ γ ∷ ώ ∷ ν ∷ ι ∷ σ ∷ μ ∷ α ∷ ι ∷ []) "2Tim.4.7"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.4.7"
  ∷ word (δ ∷ ρ ∷ ό ∷ μ ∷ ο ∷ ν ∷ []) "2Tim.4.7"
  ∷ word (τ ∷ ε ∷ τ ∷ έ ∷ ∙λ ∷ ε ∷ κ ∷ α ∷ []) "2Tim.4.7"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.4.7"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.4.7"
  ∷ word (τ ∷ ε ∷ τ ∷ ή ∷ ρ ∷ η ∷ κ ∷ α ∷ []) "2Tim.4.7"
  ∷ word (∙λ ∷ ο ∷ ι ∷ π ∷ ὸ ∷ ν ∷ []) "2Tim.4.8"
  ∷ word (ἀ ∷ π ∷ ό ∷ κ ∷ ε ∷ ι ∷ τ ∷ α ∷ ί ∷ []) "2Tim.4.8"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "2Tim.4.8"
  ∷ word (ὁ ∷ []) "2Tim.4.8"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Tim.4.8"
  ∷ word (δ ∷ ι ∷ κ ∷ α ∷ ι ∷ ο ∷ σ ∷ ύ ∷ ν ∷ η ∷ ς ∷ []) "2Tim.4.8"
  ∷ word (σ ∷ τ ∷ έ ∷ φ ∷ α ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.4.8"
  ∷ word (ὃ ∷ ν ∷ []) "2Tim.4.8"
  ∷ word (ἀ ∷ π ∷ ο ∷ δ ∷ ώ ∷ σ ∷ ε ∷ ι ∷ []) "2Tim.4.8"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "2Tim.4.8"
  ∷ word (ὁ ∷ []) "2Tim.4.8"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.4.8"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.4.8"
  ∷ word (ἐ ∷ κ ∷ ε ∷ ί ∷ ν ∷ ῃ ∷ []) "2Tim.4.8"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.4.8"
  ∷ word (ἡ ∷ μ ∷ έ ∷ ρ ∷ ᾳ ∷ []) "2Tim.4.8"
  ∷ word (ὁ ∷ []) "2Tim.4.8"
  ∷ word (δ ∷ ί ∷ κ ∷ α ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.4.8"
  ∷ word (κ ∷ ρ ∷ ι ∷ τ ∷ ή ∷ ς ∷ []) "2Tim.4.8"
  ∷ word (ο ∷ ὐ ∷ []) "2Tim.4.8"
  ∷ word (μ ∷ ό ∷ ν ∷ ο ∷ ν ∷ []) "2Tim.4.8"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.4.8"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ὶ ∷ []) "2Tim.4.8"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.4.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.8"
  ∷ word (π ∷ ᾶ ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.4.8"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Tim.4.8"
  ∷ word (ἠ ∷ γ ∷ α ∷ π ∷ η ∷ κ ∷ ό ∷ σ ∷ ι ∷ []) "2Tim.4.8"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.4.8"
  ∷ word (ἐ ∷ π ∷ ι ∷ φ ∷ ά ∷ ν ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "2Tim.4.8"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.8"
  ∷ word (Σ ∷ π ∷ ο ∷ ύ ∷ δ ∷ α ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.4.9"
  ∷ word (ἐ ∷ ∙λ ∷ θ ∷ ε ∷ ῖ ∷ ν ∷ []) "2Tim.4.9"
  ∷ word (π ∷ ρ ∷ ό ∷ ς ∷ []) "2Tim.4.9"
  ∷ word (μ ∷ ε ∷ []) "2Tim.4.9"
  ∷ word (τ ∷ α ∷ χ ∷ έ ∷ ω ∷ ς ∷ []) "2Tim.4.9"
  ∷ word (Δ ∷ η ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Tim.4.10"
  ∷ word (γ ∷ ά ∷ ρ ∷ []) "2Tim.4.10"
  ∷ word (μ ∷ ε ∷ []) "2Tim.4.10"
  ∷ word (ἐ ∷ γ ∷ κ ∷ α ∷ τ ∷ έ ∷ ∙λ ∷ ι ∷ π ∷ ε ∷ ν ∷ []) "2Tim.4.10"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ ή ∷ σ ∷ α ∷ ς ∷ []) "2Tim.4.10"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.4.10"
  ∷ word (ν ∷ ῦ ∷ ν ∷ []) "2Tim.4.10"
  ∷ word (α ∷ ἰ ∷ ῶ ∷ ν ∷ α ∷ []) "2Tim.4.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.10"
  ∷ word (ἐ ∷ π ∷ ο ∷ ρ ∷ ε ∷ ύ ∷ θ ∷ η ∷ []) "2Tim.4.10"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.4.10"
  ∷ word (Θ ∷ ε ∷ σ ∷ σ ∷ α ∷ ∙λ ∷ ο ∷ ν ∷ ί ∷ κ ∷ η ∷ ν ∷ []) "2Tim.4.10"
  ∷ word (Κ ∷ ρ ∷ ή ∷ σ ∷ κ ∷ η ∷ ς ∷ []) "2Tim.4.10"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.4.10"
  ∷ word (Γ ∷ α ∷ ∙λ ∷ α ∷ τ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.4.10"
  ∷ word (Τ ∷ ί ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.4.10"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.4.10"
  ∷ word (Δ ∷ α ∷ ∙λ ∷ μ ∷ α ∷ τ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.4.10"
  ∷ word (Λ ∷ ο ∷ υ ∷ κ ∷ ᾶ ∷ ς ∷ []) "2Tim.4.11"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.4.11"
  ∷ word (μ ∷ ό ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.4.11"
  ∷ word (μ ∷ ε ∷ τ ∷ []) "2Tim.4.11"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ῦ ∷ []) "2Tim.4.11"
  ∷ word (Μ ∷ ᾶ ∷ ρ ∷ κ ∷ ο ∷ ν ∷ []) "2Tim.4.11"
  ∷ word (ἀ ∷ ν ∷ α ∷ ∙λ ∷ α ∷ β ∷ ὼ ∷ ν ∷ []) "2Tim.4.11"
  ∷ word (ἄ ∷ γ ∷ ε ∷ []) "2Tim.4.11"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "2Tim.4.11"
  ∷ word (σ ∷ ε ∷ α ∷ υ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.11"
  ∷ word (ἔ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Tim.4.11"
  ∷ word (γ ∷ ά ∷ ρ ∷ []) "2Tim.4.11"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "2Tim.4.11"
  ∷ word (ε ∷ ὔ ∷ χ ∷ ρ ∷ η ∷ σ ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.4.11"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.4.11"
  ∷ word (δ ∷ ι ∷ α ∷ κ ∷ ο ∷ ν ∷ ί ∷ α ∷ ν ∷ []) "2Tim.4.11"
  ∷ word (Τ ∷ υ ∷ χ ∷ ι ∷ κ ∷ ὸ ∷ ν ∷ []) "2Tim.4.12"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.4.12"
  ∷ word (ἀ ∷ π ∷ έ ∷ σ ∷ τ ∷ ε ∷ ι ∷ ∙λ ∷ α ∷ []) "2Tim.4.12"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.4.12"
  ∷ word (Ἔ ∷ φ ∷ ε ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.4.12"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.4.13"
  ∷ word (φ ∷ α ∷ ι ∷ ∙λ ∷ ό ∷ ν ∷ η ∷ ν ∷ []) "2Tim.4.13"
  ∷ word (ὃ ∷ ν ∷ []) "2Tim.4.13"
  ∷ word (ἀ ∷ π ∷ έ ∷ ∙λ ∷ ι ∷ π ∷ ο ∷ ν ∷ []) "2Tim.4.13"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.4.13"
  ∷ word (Τ ∷ ρ ∷ ῳ ∷ ά ∷ δ ∷ ι ∷ []) "2Tim.4.13"
  ∷ word (π ∷ α ∷ ρ ∷ ὰ ∷ []) "2Tim.4.13"
  ∷ word (Κ ∷ ά ∷ ρ ∷ π ∷ ῳ ∷ []) "2Tim.4.13"
  ∷ word (ἐ ∷ ρ ∷ χ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.4.13"
  ∷ word (φ ∷ έ ∷ ρ ∷ ε ∷ []) "2Tim.4.13"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.13"
  ∷ word (τ ∷ ὰ ∷ []) "2Tim.4.13"
  ∷ word (β ∷ ι ∷ β ∷ ∙λ ∷ ί ∷ α ∷ []) "2Tim.4.13"
  ∷ word (μ ∷ ά ∷ ∙λ ∷ ι ∷ σ ∷ τ ∷ α ∷ []) "2Tim.4.13"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2Tim.4.13"
  ∷ word (μ ∷ ε ∷ μ ∷ β ∷ ρ ∷ ά ∷ ν ∷ α ∷ ς ∷ []) "2Tim.4.13"
  ∷ word (Ἀ ∷ ∙λ ∷ έ ∷ ξ ∷ α ∷ ν ∷ δ ∷ ρ ∷ ο ∷ ς ∷ []) "2Tim.4.14"
  ∷ word (ὁ ∷ []) "2Tim.4.14"
  ∷ word (χ ∷ α ∷ ∙λ ∷ κ ∷ ε ∷ ὺ ∷ ς ∷ []) "2Tim.4.14"
  ∷ word (π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ά ∷ []) "2Tim.4.14"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "2Tim.4.14"
  ∷ word (κ ∷ α ∷ κ ∷ ὰ ∷ []) "2Tim.4.14"
  ∷ word (ἐ ∷ ν ∷ ε ∷ δ ∷ ε ∷ ί ∷ ξ ∷ α ∷ τ ∷ ο ∷ []) "2Tim.4.14"
  ∷ word (ἀ ∷ π ∷ ο ∷ δ ∷ ώ ∷ σ ∷ ε ∷ ι ∷ []) "2Tim.4.14"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῷ ∷ []) "2Tim.4.14"
  ∷ word (ὁ ∷ []) "2Tim.4.14"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.4.14"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2Tim.4.14"
  ∷ word (τ ∷ ὰ ∷ []) "2Tim.4.14"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ α ∷ []) "2Tim.4.14"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.14"
  ∷ word (ὃ ∷ ν ∷ []) "2Tim.4.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.15"
  ∷ word (σ ∷ ὺ ∷ []) "2Tim.4.15"
  ∷ word (φ ∷ υ ∷ ∙λ ∷ ά ∷ σ ∷ σ ∷ ο ∷ υ ∷ []) "2Tim.4.15"
  ∷ word (∙λ ∷ ί ∷ α ∷ ν ∷ []) "2Tim.4.15"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Tim.4.15"
  ∷ word (ἀ ∷ ν ∷ τ ∷ έ ∷ σ ∷ τ ∷ η ∷ []) "2Tim.4.15"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Tim.4.15"
  ∷ word (ἡ ∷ μ ∷ ε ∷ τ ∷ έ ∷ ρ ∷ ο ∷ ι ∷ ς ∷ []) "2Tim.4.15"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ι ∷ ς ∷ []) "2Tim.4.15"
  ∷ word (Ἐ ∷ ν ∷ []) "2Tim.4.16"
  ∷ word (τ ∷ ῇ ∷ []) "2Tim.4.16"
  ∷ word (π ∷ ρ ∷ ώ ∷ τ ∷ ῃ ∷ []) "2Tim.4.16"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "2Tim.4.16"
  ∷ word (ἀ ∷ π ∷ ο ∷ ∙λ ∷ ο ∷ γ ∷ ί ∷ ᾳ ∷ []) "2Tim.4.16"
  ∷ word (ο ∷ ὐ ∷ δ ∷ ε ∷ ί ∷ ς ∷ []) "2Tim.4.16"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "2Tim.4.16"
  ∷ word (π ∷ α ∷ ρ ∷ ε ∷ γ ∷ έ ∷ ν ∷ ε ∷ τ ∷ ο ∷ []) "2Tim.4.16"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Tim.4.16"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.4.16"
  ∷ word (μ ∷ ε ∷ []) "2Tim.4.16"
  ∷ word (ἐ ∷ γ ∷ κ ∷ α ∷ τ ∷ έ ∷ ∙λ ∷ ι ∷ π ∷ ο ∷ ν ∷ []) "2Tim.4.16"
  ∷ word (μ ∷ ὴ ∷ []) "2Tim.4.16"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Tim.4.16"
  ∷ word (∙λ ∷ ο ∷ γ ∷ ι ∷ σ ∷ θ ∷ ε ∷ ί ∷ η ∷ []) "2Tim.4.16"
  ∷ word (ὁ ∷ []) "2Tim.4.17"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.4.17"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ό ∷ ς ∷ []) "2Tim.4.17"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "2Tim.4.17"
  ∷ word (π ∷ α ∷ ρ ∷ έ ∷ σ ∷ τ ∷ η ∷ []) "2Tim.4.17"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.17"
  ∷ word (ἐ ∷ ν ∷ ε ∷ δ ∷ υ ∷ ν ∷ ά ∷ μ ∷ ω ∷ σ ∷ έ ∷ ν ∷ []) "2Tim.4.17"
  ∷ word (μ ∷ ε ∷ []) "2Tim.4.17"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Tim.4.17"
  ∷ word (δ ∷ ι ∷ []) "2Tim.4.17"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ῦ ∷ []) "2Tim.4.17"
  ∷ word (τ ∷ ὸ ∷ []) "2Tim.4.17"
  ∷ word (κ ∷ ή ∷ ρ ∷ υ ∷ γ ∷ μ ∷ α ∷ []) "2Tim.4.17"
  ∷ word (π ∷ ∙λ ∷ η ∷ ρ ∷ ο ∷ φ ∷ ο ∷ ρ ∷ η ∷ θ ∷ ῇ ∷ []) "2Tim.4.17"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.17"
  ∷ word (ἀ ∷ κ ∷ ο ∷ ύ ∷ σ ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "2Tim.4.17"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ []) "2Tim.4.17"
  ∷ word (τ ∷ ὰ ∷ []) "2Tim.4.17"
  ∷ word (ἔ ∷ θ ∷ ν ∷ η ∷ []) "2Tim.4.17"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.17"
  ∷ word (ἐ ∷ ρ ∷ ρ ∷ ύ ∷ σ ∷ θ ∷ η ∷ ν ∷ []) "2Tim.4.17"
  ∷ word (ἐ ∷ κ ∷ []) "2Tim.4.17"
  ∷ word (σ ∷ τ ∷ ό ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.4.17"
  ∷ word (∙λ ∷ έ ∷ ο ∷ ν ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.4.17"
  ∷ word (ῥ ∷ ύ ∷ σ ∷ ε ∷ τ ∷ α ∷ ί ∷ []) "2Tim.4.18"
  ∷ word (μ ∷ ε ∷ []) "2Tim.4.18"
  ∷ word (ὁ ∷ []) "2Tim.4.18"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.4.18"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Tim.4.18"
  ∷ word (π ∷ α ∷ ν ∷ τ ∷ ὸ ∷ ς ∷ []) "2Tim.4.18"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ο ∷ υ ∷ []) "2Tim.4.18"
  ∷ word (π ∷ ο ∷ ν ∷ η ∷ ρ ∷ ο ∷ ῦ ∷ []) "2Tim.4.18"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.18"
  ∷ word (σ ∷ ώ ∷ σ ∷ ε ∷ ι ∷ []) "2Tim.4.18"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.4.18"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.4.18"
  ∷ word (β ∷ α ∷ σ ∷ ι ∷ ∙λ ∷ ε ∷ ί ∷ α ∷ ν ∷ []) "2Tim.4.18"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.18"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Tim.4.18"
  ∷ word (ἐ ∷ π ∷ ο ∷ υ ∷ ρ ∷ ά ∷ ν ∷ ι ∷ ο ∷ ν ∷ []) "2Tim.4.18"
  ∷ word (ᾧ ∷ []) "2Tim.4.18"
  ∷ word (ἡ ∷ []) "2Tim.4.18"
  ∷ word (δ ∷ ό ∷ ξ ∷ α ∷ []) "2Tim.4.18"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Tim.4.18"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Tim.4.18"
  ∷ word (α ∷ ἰ ∷ ῶ ∷ ν ∷ α ∷ ς ∷ []) "2Tim.4.18"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "2Tim.4.18"
  ∷ word (α ∷ ἰ ∷ ώ ∷ ν ∷ ω ∷ ν ∷ []) "2Tim.4.18"
  ∷ word (ἀ ∷ μ ∷ ή ∷ ν ∷ []) "2Tim.4.18"
  ∷ word (Ἄ ∷ σ ∷ π ∷ α ∷ σ ∷ α ∷ ι ∷ []) "2Tim.4.19"
  ∷ word (Π ∷ ρ ∷ ί ∷ σ ∷ κ ∷ α ∷ ν ∷ []) "2Tim.4.19"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.19"
  ∷ word (Ἀ ∷ κ ∷ ύ ∷ ∙λ ∷ α ∷ ν ∷ []) "2Tim.4.19"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.19"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Tim.4.19"
  ∷ word (Ὀ ∷ ν ∷ η ∷ σ ∷ ι ∷ φ ∷ ό ∷ ρ ∷ ο ∷ υ ∷ []) "2Tim.4.19"
  ∷ word (ο ∷ ἶ ∷ κ ∷ ο ∷ ν ∷ []) "2Tim.4.19"
  ∷ word (Ἔ ∷ ρ ∷ α ∷ σ ∷ τ ∷ ο ∷ ς ∷ []) "2Tim.4.20"
  ∷ word (ἔ ∷ μ ∷ ε ∷ ι ∷ ν ∷ ε ∷ ν ∷ []) "2Tim.4.20"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.4.20"
  ∷ word (Κ ∷ ο ∷ ρ ∷ ί ∷ ν ∷ θ ∷ ῳ ∷ []) "2Tim.4.20"
  ∷ word (Τ ∷ ρ ∷ ό ∷ φ ∷ ι ∷ μ ∷ ο ∷ ν ∷ []) "2Tim.4.20"
  ∷ word (δ ∷ ὲ ∷ []) "2Tim.4.20"
  ∷ word (ἀ ∷ π ∷ έ ∷ ∙λ ∷ ι ∷ π ∷ ο ∷ ν ∷ []) "2Tim.4.20"
  ∷ word (ἐ ∷ ν ∷ []) "2Tim.4.20"
  ∷ word (Μ ∷ ι ∷ ∙λ ∷ ή ∷ τ ∷ ῳ ∷ []) "2Tim.4.20"
  ∷ word (ἀ ∷ σ ∷ θ ∷ ε ∷ ν ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ α ∷ []) "2Tim.4.20"
  ∷ word (Σ ∷ π ∷ ο ∷ ύ ∷ δ ∷ α ∷ σ ∷ ο ∷ ν ∷ []) "2Tim.4.21"
  ∷ word (π ∷ ρ ∷ ὸ ∷ []) "2Tim.4.21"
  ∷ word (χ ∷ ε ∷ ι ∷ μ ∷ ῶ ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.4.21"
  ∷ word (ἐ ∷ ∙λ ∷ θ ∷ ε ∷ ῖ ∷ ν ∷ []) "2Tim.4.21"
  ∷ word (Ἀ ∷ σ ∷ π ∷ ά ∷ ζ ∷ ε ∷ τ ∷ α ∷ ί ∷ []) "2Tim.4.21"
  ∷ word (σ ∷ ε ∷ []) "2Tim.4.21"
  ∷ word (Ε ∷ ὔ ∷ β ∷ ο ∷ υ ∷ ∙λ ∷ ο ∷ ς ∷ []) "2Tim.4.21"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.21"
  ∷ word (Π ∷ ο ∷ ύ ∷ δ ∷ η ∷ ς ∷ []) "2Tim.4.21"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.21"
  ∷ word (Λ ∷ ί ∷ ν ∷ ο ∷ ς ∷ []) "2Tim.4.21"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.21"
  ∷ word (Κ ∷ ∙λ ∷ α ∷ υ ∷ δ ∷ ί ∷ α ∷ []) "2Tim.4.21"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Tim.4.21"
  ∷ word (ο ∷ ἱ ∷ []) "2Tim.4.21"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ὶ ∷ []) "2Tim.4.21"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Tim.4.21"
  ∷ word (Ὁ ∷ []) "2Tim.4.22"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Tim.4.22"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "2Tim.4.22"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Tim.4.22"
  ∷ word (π ∷ ν ∷ ε ∷ ύ ∷ μ ∷ α ∷ τ ∷ ό ∷ ς ∷ []) "2Tim.4.22"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "2Tim.4.22"
  ∷ word (ἡ ∷ []) "2Tim.4.22"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "2Tim.4.22"
  ∷ word (μ ∷ ε ∷ θ ∷ []) "2Tim.4.22"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Tim.4.22"
  ∷ []

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
-- There was a bug with module application in a let in a
-- parameterised module.
module Issue155 (A : Set) where

module M (Y : Set) where
  postulate F : Set → Set

Foo : Set₁
Foo = let module M′ = M A in (B : Set) → M′.F B

record R : Set₁ where
  open M A
  field
    B : Set
    C : F A

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Validity of declarative typing and kinding of Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Typing.Validity where

open import Data.Fin using (Fin; suc; zero)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Product as Prod using (∃; _,_; _×_; proj₁; proj₂)
open import Data.Vec as Vec using ([]; _∷_)
import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
open import Function using (_∘_)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε; _◅_)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Binary.TransReasoning
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contradiction)

open import FOmegaInt.Syntax
open import FOmegaInt.Typing
open import FOmegaInt.Kinding.Declarative.Equivalence
open import FOmegaInt.Reduction.Full

import FOmegaInt.Kinding.Declarative
import FOmegaInt.Kinding.Declarative.Validity

-- Extended kinding
module E where
  open FOmegaInt.Kinding.Declarative          public
  open FOmegaInt.Kinding.Declarative.Validity public
  open KindedSubstitution                     public

------------------------------------------------------------------------
-- Validity of declarative kinding, typing, subkinding and subtyping

open Syntax
open Substitution hiding (subst)
open TermCtx
open Typing
open TypedSubstitution
open WfCtxOps using (lookup-tp)

-- Validity of kinding: the kinds of well-kinded types are well-formed.
Tp∈-valid : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Tp a ∈ k → Γ ⊢ k kd
Tp∈-valid = sound-kd ∘ E.Tp∈-valid ∘ complete-Tp∈

-- Validity of subkinding: subkinds are well-formed.
<∷-valid : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j <∷ k → Γ ⊢ j kd × Γ ⊢ k kd
<∷-valid = Prod.map sound-kd sound-kd ∘ E.<∷-valid ∘ complete-<∷

-- Validity of subtyping: subtypes that are related in some kind `k'
-- inhabit `k'.
<:-valid : ∀ {n} {Γ : Ctx n} {a b k} →
           Γ ⊢ a <: b ∈ k → Γ ⊢Tp a ∈ k × Γ ⊢Tp b ∈ k
<:-valid = Prod.map sound-Tp∈ sound-Tp∈ ∘ E.<:-valid ∘ complete-<:

-- A corollary.
<:-valid-kd : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a <: b ∈ k → Γ ⊢ k kd
<:-valid-kd a<:b∈k = Tp∈-valid (proj₁ (<:-valid a<:b∈k))

-- Validity of type equality: types that are equal in some kind `k'
-- inhabit `k'.
≃-valid : ∀ {n} {Γ : Ctx n} {a b k} →
          Γ ⊢ a ≃ b ∈ k → Γ ⊢Tp a ∈ k × Γ ⊢Tp b ∈ k
≃-valid = Prod.map sound-Tp∈ sound-Tp∈ ∘ E.≃-valid ∘ complete-≃

-- Validity of kind equality: equal kinds are well-formed.
≅-valid : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ⊢ j kd × Γ ⊢ k kd
≅-valid (<∷-antisym j<∷k k<∷j) = <∷-valid j<∷k

-- Validity of combined kind and type equality: equal ascriptions are
-- well-formed.
≃wf-valid : ∀ {n} {Γ : Ctx n} {a b} →
            Γ ⊢ a ≃ b wf → Γ ⊢ a wf × Γ ⊢ b wf
≃wf-valid (≃wf-≅ j≅k)   = Prod.map wf-kd wf-kd (≅-valid j≅k)
≃wf-valid (≃wf-≃ a≃b∈k) = Prod.map wf-tp wf-tp (≃-valid a≃b∈k)

-- Validity of typing: the types of well-typed terms are well-kinded.
Tm∈-valid : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢Tm a ∈ b → Γ ⊢Tp b ∈ *
Tm∈-valid (∈-var x Γ-ctx Γ[x]≡tp-a) = lookup-tp x Γ-ctx Γ[x]≡tp-a
Tm∈-valid (∈-∀-i k-kd a∈b)    = ∈-∀-f k-kd (Tm∈-valid a∈b)
Tm∈-valid (∈-→-i a∈* b∈c c∈*) = ∈-→-f a∈* c∈*
Tm∈-valid (∈-∀-e a∈∀kc b∈k)   =
  let k-kd , c∈* = Tp∈-∀-inv (Tm∈-valid a∈∀kc)
  in Tp∈-[] c∈* (∈-tp b∈k)
Tm∈-valid (∈-→-e a∈c⇒d b∈c)   =
  let c∈* , d∈* = Tp∈-→-inv (Tm∈-valid a∈c⇒d)
  in d∈*
Tm∈-valid (∈-⇑ a∈b b<:c)      = proj₂ (<:-valid b<:c)

-- Subtypes inhabiting interval kinds are proper types.
<:-⋯-* : ∀ {n} {Γ : Ctx n} {a b c d} → Γ ⊢ a <: b ∈ c ⋯ d → Γ ⊢ a <: b ∈ *
<:-⋯-* a<:b∈c⋯d =
  let a∈c⋯d , b∈c⋯d = <:-valid a<:b∈c⋯d
  in <:-⇑ (<:-⋯-i a<:b∈c⋯d) (<∷-⋯ (<:-⊥ a∈c⋯d) (<:-⊤ b∈c⋯d))

-- An admissible rule for kinding η-expanded type operators.
Tp∈-η : ∀ {n} {Γ : Ctx n} {a j k} →
        Γ ⊢Tp a ∈ Π j k → Γ ⊢Tp Λ j (weaken a · var zero) ∈ Π j k
Tp∈-η a∈Πjk with complete-Tp∈ a∈Πjk
Tp∈-η a∈Πjk | a∈Πjk′ with E.Tp∈-valid a∈Πjk′
... | E.Kinding.kd-Π j-kd k-kd = sound-Tp∈ (E.Tp∈-η a∈Πjk′ j-kd k-kd)

-- Operations on well-formed context equality that require weakening
-- and validity of ascription equality.
module CtxEqOps where
  open Pointwise using (Pointwise; []; _∷_; map⁺)

  -- Convert a context equation to its All₂ representation.
  ≃ctx-toAll : ∀ {m} {Γ Δ : Ctx m} → Γ ≃ Δ ctx →
               Pointwise (Γ ⊢_≃_wf) (toVec Γ) (toVec Δ)
  ≃ctx-toAll ≃-[]          = []
  ≃ctx-toAll (≃-∷ a≃b Γ≃Δ) =
    let a-wf , _ = ≃wf-valid a≃b
    in ≃wf-weaken a-wf a≃b ∷ map⁺ (≃wf-weaken a-wf) (≃ctx-toAll Γ≃Δ)

  -- Ascriptions looked up in equal contexts are equal.

  lookup-≃ : ∀ {m} {Γ Δ : Ctx m} x → Γ ≃ Δ ctx →
             Γ ⊢ lookup Γ x ≃ lookup Δ x wf
  lookup-≃ x Γ≃Δ = Pointwise.lookup (≃ctx-toAll Γ≃Δ) x

  lookup-≃-kd : ∀ {m} {Γ Δ : Ctx m} {j k} x → Γ ≃ Δ ctx →
                lookup Γ x ≡ kd j → lookup Δ x ≡ kd k → Γ ⊢ j ≅ k
  lookup-≃-kd x Γ≃Δ Γ[x]≡kd-j Δ[x]≡kd-k =
    ≃wf-kd-inv (subst₂ (_ ⊢_≃_wf) Γ[x]≡kd-j Δ[x]≡kd-k (lookup-≃ x Γ≃Δ))

----------------------------------------------------------------------
-- Context narrowing (strong version)
--
-- NOTE. We could have proven a *weak* variant of context narrowing
-- for the (original) declarative judgments directly in the Typing
-- module (before establishing validity).  But since we did not need
-- (weak or strong) context narrowing of the original judgments until
-- now, it is easier to instead prove the strengthened version here
-- via context narrowing and equivalence of the extended rules.

module TypedNarrowing where

  -- Narrowing the kind of the first type variable preserves
  -- well-formedness of kinds.
  ⇓-kd : ∀ {n} {Γ : Ctx n} {j₁ j₂ k} →
         Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢ k kd → kd j₁ ∷ Γ ⊢ k kd
  ⇓-kd j₁<∷j₂ k-kd =
    let j₁<∷j₂′   = complete-<∷ j₁<∷j₂
        j₁-kd , _ = E.<∷-valid j₁<∷j₂′
    in sound-kd (E.⇓-kd j₁-kd j₁<∷j₂′ (complete-kd k-kd))

  -- Narrowing the kind of the first type variable preserves
  -- well-kindedness.
  ⇓-Tp∈ : ∀ {n} {Γ : Ctx n} {j₁ j₂ a k} →
          Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢Tp a ∈ k → kd j₁ ∷ Γ ⊢Tp a ∈ k
  ⇓-Tp∈ j₁<∷j₂ a∈k =
    let j₁<∷j₂′   = complete-<∷ j₁<∷j₂
        j₁-kd , _ = E.<∷-valid j₁<∷j₂′
    in sound-Tp∈ (E.⇓-Tp∈ j₁-kd j₁<∷j₂′ (complete-Tp∈ a∈k))

  -- Narrowing the kind of the first type variable preserves
  -- subkinding and subtyping.

  ⇓-<∷ : ∀ {n} {Γ : Ctx n} {j₁ j₂ k₁ k₂} →
         Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢ k₁ <∷ k₂ → kd j₁ ∷ Γ ⊢ k₁ <∷ k₂
  ⇓-<∷ j₁<∷j₂ k₁<∷k₂ =
    let j₁<∷j₂′   = complete-<∷ j₁<∷j₂
        j₁-kd , _ = E.<∷-valid j₁<∷j₂′
    in sound-<∷ (E.⇓-<∷ j₁-kd j₁<∷j₂′ (complete-<∷ k₁<∷k₂))

  ⇓-<: : ∀ {n} {Γ : Ctx n} {j₁ j₂ a₁ a₂ k} →
         Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢ a₁ <: a₂ ∈ k → kd j₁ ∷ Γ ⊢ a₁ <: a₂ ∈ k
  ⇓-<: j₁<∷j₂ a₁<:a₂∈k =
    let j₁<∷j₂′   = complete-<∷ j₁<∷j₂
        j₁-kd , _ = E.<∷-valid j₁<∷j₂′
    in sound-<: (E.⇓-<: j₁-kd j₁<∷j₂′ (complete-<: a₁<:a₂∈k))

open TypedNarrowing

-- Transitivity of subkinding and kind equality.
--
-- NOTE. We could have proven admissibility of these rules directly in
-- the Typing module (before establishing validity) but this would
-- have required a proof of (weak) context narrowing for the
-- (original) declarative rules.  As we do not need these transitivity
-- properties until we prove subject reduction (below), we go with an
-- indirect proof instead.

<∷-trans : ∀ {n} {Γ : Ctx n} {j k l} → Γ ⊢ j <∷ k → Γ ⊢ k <∷ l → Γ ⊢ j <∷ l
<∷-trans k₁<∷k₂ k₂<∷k₃ =
  sound-<∷ (E.<∷-trans (complete-<∷ k₁<∷k₂) (complete-<∷ k₂<∷k₃))

≅-trans : ∀ {n} {Γ : Ctx n} {j k l} → Γ ⊢ j ≅ k → Γ ⊢ k ≅ l → Γ ⊢ j ≅ l
≅-trans k₁≅k₂ k₂≅k₃ =
  sound-≅ (E.≅-trans (complete-≅ k₁≅k₂) (complete-≅ k₂≅k₃))

-- Relational reasoning for kind and type equality.
--
-- NOTE. Even though the equalities are technically preorders, we have
-- to use the weaker reasoning designed for transitive relations here.
-- This is because reflexivity proofs in typed relations are typically
-- also typed, i.e. given some context `Γ' and some raw kind or term
-- `x` we cannot, in general, conclude that `Γ ⊢ x ∼ x` without an
-- additional well-formedness proof `Γ ⊢ x' of some sort.

module ≅-Reasoning where
  ≅-reasoning : TransCtxTermRelReasoning _⊢_≅_
  ≅-reasoning = record { ∼-trans = ≅-trans }

  open TransCtxTermRelReasoning ≅-reasoning public renaming (_∼⟨_⟩_ to _≅⟨_⟩_)

module ≃-Reasoning where
  ≃-reasoning : TypedTransRelReasoning _⊢_≃_∈_
  ≃-reasoning = record { ∼-trans = ≃-trans }

  open TypedTransRelReasoning ≃-reasoning public renaming (_∼⟨_⟩_ to _≃⟨_⟩_)

----------------------------------------------------------------------
-- Generation lemmas for abstractions

-- A generation lemma for kinding of type operator abstractions.
Tp∈-Λ-inv : ∀ {n} {Γ : Ctx n} {l a j k} → Γ ⊢Tp Λ l a ∈ Π j k →
            Γ ⊢ l kd × kd j ∷ Γ ⊢Tp a ∈ k
Tp∈-Λ-inv (∈-Π-i l-kd a∈k) = l-kd , a∈k
Tp∈-Λ-inv (∈-⇑ Λl∈Πj₁k₁ (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd)) =
  let l-kd , a∈k₁ = Tp∈-Λ-inv Λl∈Πj₁k₁
  in l-kd , ∈-⇑ (⇓-Tp∈ j₂<∷j₁ a∈k₁) k₁<∷k₂

-- Term abstractions are not types.
Tp∈-¬λ : ∀ {n} {Γ : Ctx n} {a b k} → ¬ Γ ⊢Tp ƛ a b ∈ k
Tp∈-¬λ (∈-s-i λab∈c⋯d)  = Tp∈-¬λ λab∈c⋯d
Tp∈-¬λ (∈-⇑ λab∈j j<∷k) = Tp∈-¬λ λab∈j

----------------------------------------------------------------------
-- Admissible kind and type equality rules.

-- Functionality of kind formation (strong version).
kd-[≃] : ∀ {n} {Γ : Ctx n} {a b j k} →
         kd j ∷ Γ ⊢ k kd → Γ ⊢ a ≃ b ∈ j → Γ ⊢ k Kind[ a ] ≅ k Kind[ b ]
kd-[≃] k-kd a≃b∈j = sound-≅ (E.kd-[≃] (complete-kd k-kd) (complete-≃ a≃b∈j))

-- Functionality of kinding (strong version).
Tp∈-[≃] : ∀ {n} {Γ : Ctx n} {a b c j k} →
          kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢ b ≃ c ∈ j →
          Γ ⊢ a [ b ] ≃ a [ c ] ∈ k Kind[ b ]
Tp∈-[≃] a∈k b≃c∈j = sound-≃ (E.Tp∈-[≃] (complete-Tp∈ a∈k) (complete-≃ b≃c∈j))

-- An admissible congruence rule for kind equality w.r.t. dependent
-- arrow formation.
≅-Π : ∀ {n} {Γ : Ctx n} {j₁ j₂ k₁ k₂} →
      Γ ⊢ j₁ ≅ j₂ → kd j₁ ∷ Γ ⊢ k₁ ≅ k₂ → Γ ⊢ Π j₁ k₁ ≅ Π j₂ k₂
≅-Π (<∷-antisym j₁<∷j₂ j₂<∷j₁) (<∷-antisym k₁<∷k₂ k₂<∷k₁) =
  let j₁-kd , j₂-kd = <∷-valid j₁<∷j₂
      k₁-kd , k₂-kd = <∷-valid k₁<∷k₂
  in <∷-antisym (<∷-Π j₂<∷j₁ (⇓-<∷ j₂<∷j₁ k₁<∷k₂) (kd-Π j₁-kd k₁-kd))
                (<∷-Π j₁<∷j₂ k₂<∷k₁ (kd-Π j₂-kd (⇓-kd j₂<∷j₁ k₂-kd)))

-- Equal types inhabiting interval kinds are proper types.
≃-⋯-* : ∀ {n} {Γ : Ctx n} {a b c d} → Γ ⊢ a ≃ b ∈ c ⋯ d → Γ ⊢ a ≃ b ∈ *
≃-⋯-* (<:-antisym a<:b∈c⋯d b<:a∈c⋯d) =
  let a<:b∈* = <:-⋯-* a<:b∈c⋯d
      b<:a∈* = <:-⋯-* b<:a∈c⋯d
  in <:-antisym a<:b∈* b<:a∈*

-- An admissible congruence rule for type equality w.r.t. formation of
-- universal types.
≃-∀ : ∀ {n} {Γ : Ctx n} {k₁ k₂ a₁ a₂} →
      Γ ⊢ k₁ ≅ k₂ → kd k₁ ∷ Γ ⊢ a₁ ≃ a₂ ∈ * → Γ ⊢ Π k₁ a₁ ≃ Π k₂ a₂ ∈ *
≃-∀ (<∷-antisym k₁<∷k₂ k₂<∷k₁) (<:-antisym a₁<:a₂∈* a₂<:a₁∈*) =
  let k₁-kd , k₂-kd = <∷-valid k₁<∷k₂
      a₁∈*  , a₂∈*  = <:-valid a₁<:a₂∈*
  in <:-antisym (<:-∀ k₂<∷k₁ (⇓-<: k₂<∷k₁ a₁<:a₂∈*) (∈-∀-f k₁-kd a₁∈*))
                (<:-∀ k₁<∷k₂ a₂<:a₁∈* (∈-∀-f k₂-kd (⇓-Tp∈ k₂<∷k₁ a₂∈*)))

-- Another, weaker congruence lemma for type equality w.r.t. type
-- operator abstraction.
≃-λ′ : ∀ {n} {Γ : Ctx n} {j₁ j₂ a₁ a₂ k} →
       Γ ⊢ j₁ ≅ j₂ → kd j₁ ∷ Γ ⊢ a₁ ≃ a₂ ∈ k → Γ ⊢ Λ j₁ a₁ ≃ Λ j₂ a₂ ∈ Π j₁ k
≃-λ′ (<∷-antisym j₁<∷j₂ j₂<∷j₁) (<:-antisym a₁<:a₂∈k a₂<:a₁∈k) =
  let j₁-kd , j₂-kd = <∷-valid j₁<∷j₂
      a₁∈k  , a₂∈k  = <:-valid a₁<:a₂∈k
      k-kd          = Tp∈-valid a₁∈k
      k-kd′         = ⇓-kd j₂<∷j₁ k-kd
      Πj₂k<∷j₁k     = <∷-Π j₁<∷j₂ (<∷-refl k-kd) (kd-Π j₂-kd k-kd′)
      Λj₁a₁∈Πj₁k    = ∈-Π-i j₁-kd a₁∈k
      Λj₂a₂∈Πj₁k    = ∈-⇑ (∈-Π-i j₂-kd (⇓-Tp∈ j₂<∷j₁ a₂∈k)) Πj₂k<∷j₁k
  in <:-antisym (<:-λ a₁<:a₂∈k Λj₁a₁∈Πj₁k Λj₂a₂∈Πj₁k)
                (<:-λ a₂<:a₁∈k Λj₂a₂∈Πj₁k Λj₁a₁∈Πj₁k)

-- An admissible congruence rule for type equality w.r.t. type
-- application.
≃-· : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂ j k} →
      Γ ⊢ a₁ ≃ a₂ ∈ Π j k → Γ ⊢ b₁ ≃ b₂ ∈ j →
      Γ ⊢ a₁ · b₁ ≃ a₂ · b₂ ∈ k Kind[ b₁ ]
≃-· (<:-antisym a₁<:a₂∈Πjk a₂<:a₁∈Πjk) b₁≃b₂∈j with <:-valid-kd a₁<:a₂∈Πjk
... | (kd-Π j-kd k-kd) =
  <:-antisym (<:-· a₁<:a₂∈Πjk b₁≃b₂∈j)
             (<:-⇑ (<:-· a₂<:a₁∈Πjk (≃-sym b₁≃b₂∈j))
                   (≅⇒<∷ (kd-[≃] k-kd (≃-sym b₁≃b₂∈j))))

-- An admissible, more flexible β-rule for type equality.
≃-β′ : ∀ {n} {Γ : Ctx n} {a b j k l} →
       kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ j → Γ ⊢Tp Λ l a ∈ Π j k →
       Γ ⊢ (Λ l a) · b ≃ a [ b ] ∈ k Kind[ b ]
≃-β′ a∈k b∈j Λla∈Πjk =
  let j-kd = Tp∈-valid b∈j
  in ≃-trans (≃-· (≃-λ (≃-refl a∈k) Λla∈Πjk (∈-Π-i j-kd a∈k)) (≃-refl b∈j))
             (≃-β a∈k b∈j)

-- An admissible singleton-introduction rule for type equality.
≃-s-i : ∀ {n} {Γ : Ctx n} {a b c d} → Γ ⊢ a ≃ b ∈ c ⋯ d → Γ ⊢ a ≃ b ∈ a ⋯ a
≃-s-i (<:-antisym a<:b∈c⋯d b<:a∈c⋯d) =
  let a<:b∈*  = <:-⋯-* a<:b∈c⋯d
      b<:a∈*  = <:-⋯-* b<:a∈c⋯d
      a∈* , _ = <:-valid a<:b∈*
      a<:a∈*  = <:-refl a∈*
  in <:-antisym (<:-⇑ (<:-⋯-i a<:b∈c⋯d) (<∷-⋯ a<:a∈* b<:a∈*))
                (<:-⇑ (<:-⋯-i b<:a∈c⋯d) (<∷-⋯ a<:b∈* a<:a∈*))

------------------------------------------------------------------------
-- Subject reduction for kinding.

-- A variant of subject reduction for kinding: untyped β-reduction of
-- kinds and types is included in kind resp. type equality.

mutual

  kd-→β-≅ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j kd → j Kd→β k → Γ ⊢ j ≅ k
  kd-→β-≅ (kd-⋯ a∈* b∈*)   (a→a′ ⋯₁ b) = ≅-⋯ (Tp∈-→β-≃ a∈* a→a′) (≃-refl b∈*)
  kd-→β-≅ (kd-⋯ a∈* b∈*)   (a ⋯₂ b→b′) = ≅-⋯ (≃-refl a∈*) (Tp∈-→β-≃ b∈* b→b′)
  kd-→β-≅ (kd-Π j-kd k-kd) (Π₁ j→j′ k) =
    ≅-Π (kd-→β-≅ j-kd j→j′) (≅-refl k-kd)
  kd-→β-≅ (kd-Π j-kd k-kd) (Π₂ j k→k′) =
    ≅-Π (≅-refl j-kd) (kd-→β-≅ k-kd k→k′)

  Tp∈-→β-≃ : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢Tp a ∈ k → a →β b → Γ ⊢ a ≃ b ∈ k
  Tp∈-→β-≃ (∈-var x Γ-ctx Γ[x]≡kd-k) ⌈ () ⌉
  Tp∈-→β-≃ (∈-⊥-f Γ-ctx)    ⌈ () ⌉
  Tp∈-→β-≃ (∈-⊤-f Γ-ctx)    ⌈ () ⌉
  Tp∈-→β-≃ (∈-∀-f k-kd a∈*) ⌈ () ⌉
  Tp∈-→β-≃ (∈-∀-f k-kd a∈*) (Π₁ k→k′ a) =
    ≃-∀ (kd-→β-≅ k-kd k→k′) (≃-refl a∈*)
  Tp∈-→β-≃ (∈-∀-f k-kd a∈*) (Π₂ k a→a′) =
    ≃-∀ (≅-refl k-kd) (Tp∈-→β-≃ a∈* a→a′)
  Tp∈-→β-≃ (∈-→-f a∈* b∈*)  ⌈ () ⌉
  Tp∈-→β-≃ (∈-→-f a∈* b∈*)  (a→a′ ⇒₁ b) =
    ≃-→ (Tp∈-→β-≃ a∈* a→a′) (≃-refl b∈*)
  Tp∈-→β-≃ (∈-→-f a∈* b∈*)  (a ⇒₂ b→b′) =
    ≃-→ (≃-refl a∈*) (Tp∈-→β-≃ b∈* b→b′)
  Tp∈-→β-≃ (∈-Π-i j-kd a∈k) ⌈ () ⌉
  Tp∈-→β-≃ (∈-Π-i j-kd a∈k) (Λ₁ j→j′ a) =
    ≃-λ′ (kd-→β-≅ j-kd j→j′) (≃-refl a∈k)
  Tp∈-→β-≃ (∈-Π-i j-kd a∈k) (Λ₂ j a→a′) =
    ≃-λ′ (≅-refl j-kd) (Tp∈-→β-≃ a∈k a→a′)
  Tp∈-→β-≃ (∈-Π-e a∈Πjk b∈j) ⌈ cont-Tp· l a b ⌉ =
    let l-kd , a∈k = Tp∈-Λ-inv a∈Πjk
    in ≃-β′ a∈k b∈j a∈Πjk
  Tp∈-→β-≃ (∈-Π-e a∈Πjk b∈j) ⌈ cont-Tm· a b c ⌉ =
    contradiction a∈Πjk Tp∈-¬λ
  Tp∈-→β-≃ (∈-Π-e a∈Πjk b∈j) (a→a′ ·₁ b) =
    ≃-· (Tp∈-→β-≃ a∈Πjk a→a′) (≃-refl b∈j)
  Tp∈-→β-≃ (∈-Π-e a∈Πjk b∈j) (a ·₂ b→b′) =
    ≃-· (≃-refl a∈Πjk) (Tp∈-→β-≃ b∈j b→b′)
  Tp∈-→β-≃ (∈-s-i a∈k)    a→b = ≃-s-i (Tp∈-→β-≃ a∈k a→b)
  Tp∈-→β-≃ (∈-⇑ a∈j j<∷k) a→b = ≃-⇑ (Tp∈-→β-≃ a∈j a→b) j<∷k

kd-→β*-≅ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j kd → j Kd→β* k → Γ ⊢ j ≅ k
kd-→β*-≅ j-kd ε            = ≅-refl j-kd
kd-→β*-≅ j-kd (j→k ◅ k→*l) =
  let j≅k  = kd-→β-≅ j-kd j→k
      k-kd = proj₂ (≅-valid j≅k)
  in ≅-trans j≅k (kd-→β*-≅ k-kd k→*l)

Tp∈-→β*-≃ : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢Tp a ∈ k → a →β* b → Γ ⊢ a ≃ b ∈ k
Tp∈-→β*-≃ a∈k ε            = ≃-refl a∈k
Tp∈-→β*-≃ a∈k (a→b ◅ b→*c) =
  let a≃b∈k = Tp∈-→β-≃ a∈k a→b
      b∈k   = proj₂ (≃-valid a≃b∈k)
  in ≃-trans a≃b∈k (Tp∈-→β*-≃ b∈k b→*c)

-- A corollary: subject reduction for kinding, aka preservation of
-- kinding under (full) β-reduction.
pres-Tp∈-→β* : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢Tp a ∈ k → a →β* b → Γ ⊢Tp b ∈ k
pres-Tp∈-→β* a∈k a→b = proj₂ (≃-valid (Tp∈-→β*-≃ a∈k a→b))

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
module Foundation.Semigroup where

open import Foundation.Primitive
open import Foundation.Equivalence
open import Agda.Primitive

record IsAssociative {a} {A : Set a} {ℓ} ⦃ _ : Equivalence A ℓ ⦄ (_∙_ : A → A → A) : ℞ a ⊔ ℓ where
  field
    associativity : ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

open IsAssociative ⦃ … ⦄

record Semigroup {c} (A : Set c) ℓ : Set (c ⊔ ⟰ ℓ) where
  field
    ⦃ equivalence ⦄ : Equivalence A ℓ
    _∙_ : A → A → A
    isAssociative : IsAssociative _∙_

open Semigroup ⦃ … ⦄

record Monoid {a} (A : Set a) ℓ : Set (a ⊔ ⟰ ℓ) where
  field
    ⦃ semigroup ⦄ : Semigroup A ℓ
    ε : A
    left-identity : ∀ x → ε ∙ x ≈ x
    right-identity : ∀ x → x ∙ ε ≈ x

open Monoid ⦃ … ⦄

open import Relation.Binary.Core
open import Algebra.FunctionProperties.Core

PowerRightIdentity : ∀ {a ℓ} {A : Set a} → Rel A ℓ → ∀ {b} {B : Set b} → B → (B → A → A) → Set _
PowerRightIdentity _≈_ e _◃_ = ∀ x → (e ◃ x) ≈ x

PowerAssociative : ∀ {a b ℓ} {A : Set a} {B : Set b} → (A → A → Set ℓ) → (B → A → A) → (B → B → B) → Set _
PowerAssociative _≈_ _◃_ _∙_ = ∀ x a b → ((b ∙ a) ◃ x) ≈ (b ◃ (a ◃ x))

_over_ : ∀ {f} {F : Set f} {g} → (F → F → Set g) → ∀ {i} {I : Set i} {a} {A : Set a} → (A → I → F) → A → A → Set (i ⊔ g)
_*_ over f = λ x y → ∀ i → f x i * f y i

record IsMonoidTransformer {s ℓˢ} {S : Set s} (≈ˢ : Rel S ℓˢ) {m ℓᵐ} {M : Set m} (≈ᵐ : Rel M ℓᵐ) (∙ : Op₂ M) (ε : M) (◃ : M → S → S) : Set (s ⊔ ℓˢ ⊔ m ⊔ ℓᵐ) where
  field
    ◃-identity : PowerRightIdentity ≈ˢ ε ◃
    ≈ˢ-over-◃-⟶-≈ᵐ : ≈ˢ over ◃ ⇒ ≈ᵐ
    ≈ᵐ-to-≈ˢ-over-◃ : ≈ᵐ ⇒ ≈ˢ over ◃
    ◃-extracts-∙ : PowerAssociative ≈ˢ ◃ ∙

open IsMonoidTransformer ⦃ … ⦄

record MonoidTransformer {s} (S : Set s) ℓˢ {m} (M : Set m) ℓᵐ : Set (s ⊔ m ⊔ lsuc (ℓˢ ⊔ ℓᵐ)) where
  field
    ⦃ base ⦄ : Equivalence S ℓˢ
    ⦃ exponent ⦄ : Monoid M ℓᵐ

  infixl 6 _◃_
  field
    _◃_ : M → S → S
    instance isMonoidTransformer : IsMonoidTransformer _≈_ _≈_ _∙_ ε _◃_


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.List.Base where

open import Agda.Builtin.List        public
open import Cubical.Core.Everything
open import Cubical.Data.Maybe.Base
open import Cubical.Data.Nat.Base

module _ {ℓ} {A : Type ℓ} where

  infixr 5 _++_
  infixl 5 _∷ʳ_

  [_] : A → List A
  [ a ] = a ∷ []

  _++_ : List A → List A → List A
  [] ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ xs ++ ys

  rev : List A → List A
  rev [] = []
  rev (x ∷ xs) = rev xs ++ [ x ]

  _∷ʳ_ : List A → A → List A
  xs ∷ʳ x = xs ++ x ∷ []

  length : List A → ℕ
  length [] = 0
  length (x ∷ l) = 1 + length l

  map : ∀ {ℓ'} {B : Type ℓ'} → (A → B) → List A → List B
  map f [] = []
  map f (x ∷ xs) = f x ∷ map f xs

  map2 : ∀ {ℓ' ℓ''} {B : Type ℓ'} {C : Type ℓ''}
    → (A → B → C) → List A → List B → List C
  map2 f [] _ = []
  map2 f _ [] = []
  map2 f (x ∷ xs) (y ∷ ys) = f x y ∷ map2 f xs ys

  foldr : ∀ {ℓ'} {B : Type ℓ'} → (A → B → B) → B → List A → B
  foldr f b [] = b
  foldr f b (x ∷ xs) = f x (foldr f b xs)

  foldl : ∀ {ℓ'} {B : Type ℓ'} → (B → A → B) → B → List A → B
  foldl f b [] = b
  foldl f b (x ∷ xs) = foldl f (f b x) xs

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module Instances where

open import Level using () renaming (zero to ℓ₀)
open import Category.Functor using (RawFunctor)
open import Data.Maybe as M using (Maybe)
open import Data.Nat using (ℕ)
open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
open import Data.Vec using (Vec)
import Data.Vec.Equality
open Data.Vec.Equality.PropositionalEquality using () renaming (to-≡ to VecEq-to-≡)
open import Function using (_∘_ ; id)
open import Relation.Binary using (Setoid ; module Setoid)
open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning)

open Setoid using () renaming (_≈_ to _∋_≈_)

open import Generic using (VecISetoid)
open import Structures using (Functor ; Shaped ; module Shaped)

MaybeFunctor : Functor Maybe
MaybeFunctor = record
  { rawfunctor = M.functor
  ; isFunctor = record
    { cong = cong
    ; identity = identity
    ; composition = composition
    } }
  where _<$>_ : {α β : Set} → (α → β) → Maybe α → Maybe β
        _<$>_ = RawFunctor._<$>_ M.functor

        cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h
        cong g≗h (M.just x) = P.cong M.just (g≗h x)
        cong g≗h M.nothing  = P.refl

        identity : {α : Set} → _<$>_ {α} id ≗ id
        identity (M.just x) = P.refl
        identity M.nothing  = P.refl

        composition : {α β γ : Set} → (g : β → γ) → (h : α → β) → _<$>_ (g ∘ h) ≗ _<$>_ g ∘ _<$>_ h
        composition g h (M.just x) = P.refl
        composition g h M.nothing  = P.refl

VecShaped : Shaped ℕ Vec
VecShaped = record
  { arity = id
  ; content = id
  ; fill = λ _ → id
  ; isShaped = record
    { content-fill = λ _ → P.refl
    ; fill-content = λ _ _ → P.refl
    } }

ShapedISetoid : (S : Setoid ℓ₀ ℓ₀) {C : Set → (Setoid.Carrier S) → Set} → Shaped (Setoid.Carrier S) C → Setoid ℓ₀ ℓ₀ → ISetoid (Setoid.Carrier S) ℓ₀ ℓ₀
ShapedISetoid S {C} ShapeT α = record
  { Carrier = C (Setoid.Carrier α)
  ; _≈_ = λ {s₁} {s₂} c₁ c₂ → S ∋ s₁ ≈ s₂ × ISetoid._≈_ (VecISetoid α) (content c₁) (content c₂)
  ; isEquivalence = record
    { refl = Setoid.refl S , ISetoid.refl (VecISetoid α)
    ; sym = λ p → Setoid.sym S (proj₁ p) , ISetoid.sym (VecISetoid α) (proj₂ p)
    ; trans = λ p q → Setoid.trans S (proj₁ p) (proj₁ q) , ISetoid.trans (VecISetoid α) (proj₂ p) (proj₂ q)
    } } where open Shaped ShapeT

Shaped≈-to-≡ : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Set) → {s : S} {x y : C α s} → ShapedISetoid (P.setoid S) ShapeT (P.setoid α) at s ∋ x ≈ y → x ≡ y
Shaped≈-to-≡ ShapeT α {s} {x} {y} (shape≈ , content≈) = begin
  x
    ≡⟨ P.sym (content-fill x) ⟩
  fill s (content x)
    ≡⟨ P.cong (fill s) (VecEq-to-≡ content≈) ⟩
  fill s (content y)
    ≡⟨ content-fill y ⟩
  y ∎
  where open ≡-Reasoning
        open Shaped ShapeT

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Rationals.HITQ where

open import Cubical.HITs.Rationals.HITQ.Base public

-- open import Cubical.HITs.Rationals.HITQ.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Data.Fin.Base where

open import Data.Maybe.Base
open import Data.Nat.Base using (ℕ; suc; zero)
open import Level
open import Data.Empty

Fin : ℕ → Type
Fin zero    = ⊥
Fin (suc n) = Maybe (Fin n)

pattern f0 = nothing
pattern fs n = just n

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- This file contains the definition of a preorder as a category with --
-- additional properties.                                             --
------------------------------------------------------------------------
module Category.Preorder where

open import Level renaming (suc to lsuc)
open import Data.Empty

open import Setoid.Total
open import Category.Category
open import Equality.Eq

record PO {l : Level} : Set (lsuc l) where
  field
    -- The underlying category.
    ℙ : Cat {l}

    -- The preorder axiom.
    POax : ∀{A B}{f g : el (Hom ℙ A B)} → ⟨ Hom ℙ A B ⟩[ f ≡ g ]

open PO public renaming (ℙ to po-cat)

-- A PO with 4 objects.
module 4PO where
    -- The objects.
    data 4Obj {l : Level} : Set l where
      i₁ : 4Obj
      i₂ : 4Obj
      i₃ : 4Obj
      i₄ : 4Obj

    -- The PreHom.
    data 4PHom {l : Level} : 4Obj {l} → 4Obj {l} → Set l where
      id₁ : 4PHom i₁ i₁
      f₁ : 4PHom i₁ i₂
      f₂ : 4PHom i₁ i₃
      id₂ : 4PHom i₂ i₂
      f₃ : 4PHom i₂ i₄
      id₃ : 4PHom i₃ i₃
      f₄ : 4PHom i₃ i₄
      f₅ : 4PHom i₁ i₄
      id₄ : 4PHom i₄ i₄

    -- The Hom.
    4Hom : {l : Level} → 4Obj {l} → 4Obj {l} → Setoid {l}
    4Hom i₁ i₁ = record { el = 4PHom i₁ i₁; eq = λ a b → a ≅ b; eqRpf = isEqRel }
    4Hom i₁ i₂ = record { el = 4PHom i₁ i₂; eq = λ a b → a ≅ b; eqRpf = isEqRel }
    4Hom i₁ i₃ = record { el = 4PHom i₁ i₃; eq = λ a b → a ≅ b; eqRpf = isEqRel }
    4Hom i₁ i₄ = record { el = 4PHom i₁ i₄; eq = λ a b → a ≅ b; eqRpf = isEqRel }
    4Hom i₂ i₂ = record { el = 4PHom i₂ i₂; eq = λ a b → a ≅ b; eqRpf = isEqRel }
    4Hom i₂ i₄ = record { el = 4PHom i₂ i₄; eq = λ a b → a ≅ b; eqRpf = isEqRel }
    4Hom i₃ i₃ = record { el = 4PHom i₃ i₃; eq = λ a b → a ≅ b; eqRpf = isEqRel }
    4Hom i₃ i₄ = record { el = 4PHom i₃ i₄; eq = λ a b → a ≅ b; eqRpf = isEqRel }
    4Hom i₄ i₄ = record { el = 4PHom i₄ i₄; eq = λ a b → a ≅ b; eqRpf = isEqRel }
    4Hom  _  _ = EmptySetoid

    4Comp : {l : Level}{a b c : 4Obj {l}} → BinSetoidFun (4Hom a b) (4Hom b c) (4Hom a c)
    4Comp {_} {i₁} {i₂} {i₁} = record { appT = λ x → record { appT = λ x₁ → id₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₁} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₂} {i₁} {i₂} = record { appT = λ x → record { appT = λ x₁ → id₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₁} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₂} {i₁} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₁} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₃} {i₂} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₁} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₃} {i₁} {i₃} = record { appT = λ x → record { appT = λ x₁ → id₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₁} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₄} {i₁} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₄} {i₂} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₄} {i₁} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₄} {i₁} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₄} {i₃} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₄} {i₁} {i₄} = record { appT = λ x → record { appT = λ x₁ → ⊥-poly-elim x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₄} {i₄} {i₃} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₄} {i₄} {i₂} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₄} {i₄} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₄} {i₃} {i₄} = record { appT = λ x → record { appT = λ x₁ → id₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₄} {i₃} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₄} {i₃} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₄} {i₂} {i₄} = record { appT = λ x → record { appT = λ x₁ → id₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₄} {i₂} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₄} {i₂} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₃} {i₄} {i₃} = record { appT = λ x → record { appT = λ x₁ → id₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₄} {i₂} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₄} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₃} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₃} {i₂} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₃} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₂} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₂} {i₃} = record { appT = λ x → record { appT = λ x₁ → id₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₃} {i₂} {i₂} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₃} {i₄} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₄; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₄} {i₃} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₄} {i₂} = record { appT = λ x → record { appT = λ x₁ → id₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₄} {i₁} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₃} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₃; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₃} {i₂} = record { appT = λ x → record { appT = λ x₁ → id₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₃} {i₁} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₂} {i₂} {i₄} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₂} {i₃} = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₂} {i₂} = record { appT = λ x → record { appT = λ x₁ → id₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₂} {i₃} {i₃} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₂} {i₄} {i₄} = record { appT = λ x → record { appT = λ x₁ → x; extT = λ x₂ → refl }; extT = λ x₁ x₂ → x₁ }
    4Comp {_} {i₁} {i₄} {i₃} = record { appT = λ x → record { appT = λ x₁ → f₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₄} {i₂} = record { appT = λ x → record { appT = λ x₁ → f₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₄} {i₁} = record { appT = λ x → record { appT = λ x₁ → id₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₃} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₅; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₃} {i₂} = record { appT = λ x → record { appT = λ x₁ → f₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₃} {i₁} = record { appT = λ x → record { appT = λ x₁ → id₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₂} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₅; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₂} {i₃} = record { appT = λ x → record { appT = λ x₁ → f₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₂} {i₂} = record { appT = λ x → record { appT = λ x₁ → f₁; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₃} {i₃} = record { appT = λ x → record { appT = λ x₁ → f₂; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {_} {i₁} {i₄} {i₄} = record { appT = λ x → record { appT = λ x₁ → f₅; extT = λ x₂ → refl }; extT = λ x₁ x₂ → refl }
    4Comp {l} {i₁} {i₁} {c}  = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refPf (eqRpf (4Hom i₁ c)) {x₂} }
    4Comp {l} {i₂} {i₂} {c}  = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refPf (eqRpf (4Hom i₂ c)) {x₂} }
    4Comp {l} {i₃} {i₃} {c}  = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refPf (eqRpf (4Hom i₃ c)) {x₂} }
    4Comp {l} {i₄} {i₄} {c}  = record { appT = λ x → record { appT = λ x₁ → x₁; extT = λ x₂ → x₂ }; extT = λ x₁ x₂ → refPf (eqRpf (4Hom i₄ c)) {x₂} }

    4Id : {l : Level}{A : 4Obj {l}} → el (4Hom A A)
    4Id {_}{i₁} = id₁
    4Id {_}{i₂} = id₂
    4Id {_}{i₃} = id₃
    4Id {_}{i₄} = id₄

    4PO-ax : ∀{l}{A B : 4Obj {l}}{f g : el (4Hom A B)} → eq (4Hom A B) f g
    4PO-ax {A = i₁} {i₁} {id₁} {id₁} = refl
    4PO-ax {A = i₁} {i₂} {f₁}  {f₁}  = refl
    4PO-ax {A = i₁} {i₃} {f₂}  {f₂}  = refl
    4PO-ax {A = i₁} {i₄} {f₅}  {f₅}  = refl
    4PO-ax {A = i₂} {i₂} {id₂} {id₂} = refl
    4PO-ax {A = i₂} {i₄} {f₃}  {f₃}  = refl
    4PO-ax {A = i₃} {i₃} {id₃} {id₃} = refl
    4PO-ax {A = i₃} {i₄} {f₄}  {f₄}  = refl
    4PO-ax {A = i₄} {i₄} {id₄} {id₄} = refl
    4PO-ax {A = i₂} {i₁} {f}         = ⊥-poly-elim f
    4PO-ax {A = i₃} {i₁} {f}         = ⊥-poly-elim f
    4PO-ax {A = i₄} {i₁} {f}         = ⊥-poly-elim f
    4PO-ax {A = i₃} {i₂} {f}         = ⊥-poly-elim f
    4PO-ax {A = i₄} {i₂} {f}         = ⊥-poly-elim f
    4PO-ax {A = i₂} {i₃} {f}         = ⊥-poly-elim f
    4PO-ax {A = i₄} {i₃} {f}         = ⊥-poly-elim f

    4AssocPf : ∀{l}{A B C D : 4Obj {l}} {f : el (4Hom A B)} {g : el (4Hom B C)}{h : el (4Hom C D)}
      → ⟨ 4Hom A D ⟩[ f ○[ 4Comp {l} {A}{B}{D} ] (g ○[ 4Comp {l}{B}{C}{D} ] h) ≡ (f ○[ 4Comp {l} {A}{B}{C} ] g) ○[ 4Comp {l}{A}{C}{D} ] h ]
    4AssocPf {l}{A}{B}{C}{D} {f}{g} = 4PO-ax {l} {A} {D}

    4IdPF : {l : Level}{A B : 4Obj {l}} {f : el (4Hom A B)}
      → ⟨ 4Hom A B ⟩[ (4Id {l}{A}) ○[ 4Comp {l}{A}{A}{B} ] f ≡ f ○[ 4Comp {l}{A}{B}{B} ] (4Id {l}{B}) ]
    4IdPF {l}{A}{B}{f} = 4PO-ax {l} {A} {B}

    -- We have a category.
    4cat : {l : Level} → Cat {l}
    4cat {l} = record { Obj = 4Obj {l};
                        Hom = 4Hom;
                       comp = λ {A} {B} {C} → 4Comp {l} {A}{B}{C};
                         id = λ {A} → 4Id {l}{A};
                    assocPf = λ {A} {B} {C} {D} {f} {g} {h} → 4AssocPf {l}{A}{B}{C}{D}{f}{g}{h};
                       idPfCom = λ {A} {B} {f} → 4IdPF {l}{A}{B}{f};
                       idPf = λ {A} {B} {f} → 4PO-ax {l} {A} {B}}

    -- We have a preorder.
    4po : {l : Level} → PO {l}
    4po {l} = record { ℙ = 4cat;
                    POax = λ {A} {B} {f} {g} → 4PO-ax {l} {A} {B} {f} {g} }

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
module BasicIS4.Metatheory.Hilbert-TarskiGluedHilbert where

open import BasicIS4.Syntax.Hilbert public
open import BasicIS4.Semantics.TarskiGluedHilbert public

-- Internalisation of syntax as syntax representation in a particular model.

module _ {{_ : Model}} where
  [_] : ∀ {A Γ} → Γ ⊢ A → Γ [⊢] A
  [ var i ]   = [var] i
  [ app t u ] = [app] [ t ] [ u ]
  [ ci ]      = [ci]
  [ ck ]      = [ck]
  [ cs ]      = [cs]
  [ box t ]   = [box] [ t ]
  [ cdist ]   = [cdist]
  [ cup ]     = [cup]
  [ cdown ]   = [cdown]
  [ cpair ]   = [cpair]
  [ cfst ]    = [cfst]
  [ csnd ]    = [csnd]
  [ unit ]    = [unit]

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)           γ = lookup i γ
eval (app {A} {B} t u) γ = _⟪$⟫_ {A} {B} (eval t γ) (eval u γ)
eval ci                γ = K I
eval (ck {A} {B})      γ = K (⟪K⟫ {A} {B})
eval (cs {A} {B} {C})  γ = K (⟪S⟫′ {A} {B} {C})
eval (box t)           γ = K ([ box t ] ⅋ eval t ∙)
eval cdist             γ = K _⟪D⟫′_
eval cup               γ = K ⟪↑⟫
eval cdown             γ = K ⟪↓⟫
eval (cpair {A} {B})   γ = K (_⟪,⟫′_ {A} {B})
eval cfst              γ = K π₁
eval csnd              γ = K π₂
eval unit              γ = ∙

-- TODO: Correctness of evaluation with respect to conversion.

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { _⊩ᵅ_    = λ Γ P → Γ ⊢ α P
      ; mono⊩ᵅ  = mono⊢
      ; _[⊢]_   = _⊢_
      ; mono[⊢] = mono⊢
      ; [var]    = var
      ; [app]    = app
      ; [ci]     = ci
      ; [ck]     = ck
      ; [cs]     = cs
      ; [box]    = box
      ; [cdist]  = cdist
      ; [cup]    = cup
      ; [cdown]  = cdown
      ; [cpair]  = cpair
      ; [cfst]   = cfst
      ; [csnd]   = csnd
      ; [unit]   = unit
      }

-- Soundness and completeness with respect to the canonical model.

mutual
  reflectᶜ : ∀ {A Γ} → Γ ⊢ A → Γ ⊩ A
  reflectᶜ {α P}   t = t
  reflectᶜ {A ▻ B} t = λ η → let t′ = mono⊢ η t
                              in  λ a → reflectᶜ (app t′ (reifyᶜ a))
  reflectᶜ {□ A}   t = λ η → let t′ = mono⊢ η t
                              in  t′ ⅋ reflectᶜ (down t′)
  reflectᶜ {A ∧ B} t = reflectᶜ (fst t) , reflectᶜ (snd t)
  reflectᶜ {⊤}    t = ∙

  reifyᶜ : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ A
  reifyᶜ {α P}   s = s
  reifyᶜ {A ▻ B} s = lam (reifyᶜ (s weak⊆ (reflectᶜ {A} v₀)))
  reifyᶜ {□ A}   s = syn (s refl⊆)
  reifyᶜ {A ∧ B} s = pair (reifyᶜ (π₁ s)) (reifyᶜ (π₂ s))
  reifyᶜ {⊤}    s = unit

reflectᶜ⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ Ξ → Γ ⊩⋆ Ξ
reflectᶜ⋆ {∅}     ∙        = ∙
reflectᶜ⋆ {Ξ , A} (ts , t) = reflectᶜ⋆ ts , reflectᶜ t

reifyᶜ⋆ : ∀ {Ξ Γ} → Γ ⊩⋆ Ξ → Γ ⊢⋆ Ξ
reifyᶜ⋆ {∅}     ∙        = ∙
reifyᶜ⋆ {Ξ , A} (ts , t) = reifyᶜ⋆ ts , reifyᶜ t

-- Reflexivity and transitivity.

refl⊩⋆ : ∀ {Γ} → Γ ⊩⋆ Γ
refl⊩⋆ = reflectᶜ⋆ refl⊢⋆

trans⊩⋆ : ∀ {Γ Γ′ Γ″} → Γ ⊩⋆ Γ′ → Γ′ ⊩⋆ Γ″ → Γ ⊩⋆ Γ″
trans⊩⋆ ts us = reflectᶜ⋆ (trans⊢⋆ (reifyᶜ⋆ ts) (reifyᶜ⋆ us))

-- Completeness with respect to all models, or quotation.

quot : ∀ {A Γ} → Γ ⊨ A → Γ ⊢ A
quot s = reifyᶜ (s refl⊩⋆)

-- Normalisation by evaluation.

norm : ∀ {A Γ} → Γ ⊢ A → Γ ⊢ A
norm = quot ∘ eval

-- TODO: Correctness of normalisation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module HelloWorldPrim where

open import IO.Primitive.Infinite
open import Codata.Musical.Costring

main = putStrLn (toCostring "Hello World!")

max_stars_repo_name: ashinkarov/agda

max_issues_repo_name: ashinkarov/agda

max_forks_repo_name: ashinkarov/agda


text:
postulate
  A B : Set
  C : .{{_ : B}} → Set
  instance
    f : {{_ : A}} → B
  test : {{x : A}} → C